Constructing Induction Rules for Deductive Synthesis Proofs

We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof, but standard techniques for the construction of appropriate induction rules are restricted to recycling the recursive structure of the specifications. What is needed is induction rule construction techniques that can introduce novel recursive structures. We show that a combination of rippling and the use of meta-variables as a least-commitment device can provide such novelty.     

Recursive Program Optimization through Inductive Synthesis Proof Transformation

The research described in this paper involved developing transformation techniques that increase the efficiency of the original program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation system that, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation and highlight the benefits of proof transformation with regards to search, correctness, automatability, and generality.     

Verification of object-oriented programs: A transformational approach

We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters. We also explain how the transformational approach can be extended to deal with other features of object-oriented programming, like classes, inheritance, subtyping and dynamic binding.     

Proofs, Programs, Processes

The objective of this paper is to provide a theoretical foundation for program extraction from inductive and coinductive proofs geared to practical applications. The novelties consist in the addition of inductive and coinductive definitions to a realizability interpretation for first-order proofs, a soundness proof for this system, and applications to the synthesis of non-trivial provably correct programs in the area of exact real number computation. We show that realizers, although per se untyped, can be assigned polymorphic recursive types and hence represent valid programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t. the binary signed digit representation.     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

A Syntactic Approach to Foundational Proof-Carrying Code

Proof-carrying code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. In foundational proof-carrying code (FPCC), on the other hand, proofs are constructed and verified by using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base. Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and recursive types. In this article, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker, while the latter is known to be much easier to construct than the semantic soundness proofs. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system through an implementation in the Coq proof assistant.     

Recursive assertions and parallel programs

Summary We prove that recursive assertions are enough for proofs of parallel programs considered in Owicki and Gries [7]. In other words, we prove that for any parallel program S and recursive assertions p and q if {p} S{q} is true under the standard interpretation in natural numbers then all intermediate assertions needed in the proof can be chosen recursive. Finally, we show that if auxiliary variables are used only as program counters then the above result does not hold.     

Proof by analogy in mural

An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct? One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming. This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.     

Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis

The structured programming literature provides methods and a wealth of heuristic knowledge for guiding the construction of provably correct imperative programs. We investigate these methods and heuristics as a basis for mechanizing program synthesis. Our approach combines proof planning with conventional partial order planning. Proof planning is an automated theorem proving technique which uses high-level proof plans to guide the search for proofs. Proof plans are structured in terms of proof methods, which encapsulate heuristics for guiding proof search. We demonstrate that proof planning provides a local perspective on the synthesis task. In particular, we show that proof methods can be extended to represent heuristics for guiding program construction. Partial order planning complements proof planning by providing a global perspective on the synthesis task. This means that it allows us to reason about the order in which program fragments are composed. Our hybrid approach has been implemented in a semi-automatic system called Bertha. Bertha supports partial correctness and has been tested on a wide range of non-trivial programming examples.     

Termination of Nested and Mutually Recursive Algorithms

This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion.We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthys f_91 function).     

Studies of a Theory of Specifications with Built-in Program Extraction

We present a Theory of Specifications based on Martin-Löf's type theory, with rules for simultaneously constructing programs and their correctness proofs. The theory contains types for representing specifications whose corresponding notion of implementation is that of a pair formed by a program and a correctness proof. The rules of the theory are such that in implementations the program parts appear mixed together with the proof parts. A confluent and normalizing computational relation performs the task of separating programs from proofs. As a consequence, every implementation computes to a pair composed of a program and a proof of its correctness, and so the program extraction procedure is immediate.     

A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs

This paper is concerned with a proof-theoretic observation about two kinds of proof systems for regular cyclic objects. It is presented for the case of two formal systems that are complete with respect to the notion of “recursive type equality” on a restricted class of recursive types in μ-term notation. Here we show the existence of an immediate duality with a geometrical visualization between proofs in a variant of the coinductive axiom system due to Brandt and Henglein and “consistency-unfoldings” in a variant of a 'syntactic-matching' proof system for testing equations between recursive types due to Ariola and Klop.Finally we sketch an analogous result of a duality between a similar pair of proof systems for bisimulation equivalence on equational specifications of cyclic term graphs.     

Certifying Term Rewriting Proofs in ELAN

Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions (ρσ-calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity).     

Proving the Correctness of Multiprocess Programs

The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs. Individual processes are represented by ordinary flowcharts, and no special synchronization mechanisms are assumed, so the method can be applied to a large class of multiprocess programs. A correctness proof can be designed together with the program by a hierarchical process of stepwise refinement, making the method practical for larger programs. The resulting proofs tend to be natural formalizations of the informal proofs that are now used.     

Using Computer Algebra techniques for the specification,verification and synthesis of recursive programs

We describe an innovative method for proving total correctness of tail recursive programs having a specific structure, namely programs in which an auxiliary tail recursive function is driven by a main nonrecursive function, and only the specification of the main function is provided. The specification of the auxiliary function is obtained almost fully automatically by solving coupled linear recursive sequences with constant coefficients. The process is carried out by means of CA (Computer Algebra) and AC (Algorithmic Combinatorics) and is implemented in the Theorema system (using Mathematica). We demonstrate this method on an example involving polynomial expressions. Furthermore, we develop a method for synthesis of recursive programs for computing polynomial expressions of a fixed degree by means of “cheap” operations, e.g., additions, subtractions and multiplications. For a given polynomial expression, we define its recursive program in a schemewise manner. The correctness of the synthesized programs follows from the general correctness of the synthesis method, which is proven once for all, using the verification method presented in the first part of this paper.     

A shared-variable concurrency analysis of multi-threaded object-oriented programs

In this paper a proof outline logic is introduced for the partial correctness of multi-threaded object-oriented programs like in Java. The main contribution is a generalization of the Owicki& Gries proof method for shared-variable concurrency to dynamic thread creation. This paper also provides a formal justification of this generalization in terms of soundness and completeness proofs.     

New uses of linear arithmetic in automated theorem proving by induction

Zhang, Kapur, and Krishnamoorthy introduced a cover set method for designing induction schemes for automating proofs by induction from specifications expressed as equations and conditional equations. This method has been implemented in the theorem prover Rewrite Rule Laboratory (RRL) and a proof management system Tecton built on top of RRL, and it has been used to prove many nontrivial theorems and reason about sequential as well as parallel programs. The cover set method is based on the assumption that a function symbol is defined by using a finite set of terminating (conditional or unconditional) rewrite rules. The termination ordering employed in orienting the rules is used to perform proofs by well-founded induction. The left sides of the rules are used to design different cases of an induction sheme, and recursive calls to the function made in the right side can be used to design appropriate instantiations for generating induction hypotheses. A weakness of this method is that it relies on syntactic unification for generating an induction scheme for a conjecture. This paper goes a step further by proposing semantic analysis for generating an induction scheme for a conjecture from a cover set. We discuss the use of a decision procedure for Presburger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ⩾, ⩽) for performing semantic analysis about numbers. The decision procedure is used to generate appropriate induction schemes for a conjecture by using cover sets of function taking numbers as arguments. This extension of the cover set method automates proofs of many theorems that otherwise require human guidance and hints. The effectiveness of the method is demonstrated by using some examples that commonly arise in reasoning about specifications and programs. It is also shown how semantic analysis using a Presburger arithmetic decision procedure can be used for checking the completeness of a cover set of a function defined by using operations such as + and — on numbers. With this check, many function definitions used in a proof of the prime factorization theorem stating that every number can be factored uniquely into prime factors, which had to be checked manually, an now be checked automatically in RRL. The use of the decision procedure for guiding generalization for generating conjectures and merging induction schemes is also illustrated. Partially supported by the National Science Foundation Grant No. CCR-9303394 and subcontract CB0249 of SRI contract MDA904-92-C-5186 with The Maryland Procurement Office.     

Termination of String Rewriting Proved Automatically

This paper describes how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method, and semantic labelling can be used for automatically proving termination of an extensive class of string rewriting systems (SRSs). The tool implementing this combination of techniques is called TORPA: Termination of Rewriting Proved Automatically. All termination proofs generated by TORPA are easy to read and check; but for many of the SRSs involved, finding a termination proof would be a hard job for a human. This paper contains all underlying theory, describes how the search for a termination proof is implemented, and includes many examples.