Ch I is an introduction to program verification and contains an abstract which is translated in english below.
Ch. 2 is devoted to the study of the operational semantics of programs.
All program proof methods use the notion of "program step". This naturally leads to the formalization of the semantics of a program by a transition system (Sect. 2.2) given by a set of states (in general a pair memory state - control state), a set of actions, a characterization of the initial states and a transition relation which for any action"a" characterizes the pairs of states "s" and "s'" such that by executing action "a" in state "S", one can reach the successor state "s'" in one computation step.
The semantics generated by the transition system (Sect. 2.4) is given by the set of states, actions and traces generated by this transitions system. A trace is a sequence of states separated by actions (according to the transition relation) which starts by an initial state and is infinite or else terminates by a blocking state (without possible successor). Thus traces represent a completed finite computation or an infinite computation but never a partial computation.
Unfortunately not all program semantics are directly generated by a transition system. For example, this is the case of the the semantics of fair parallel programs since the computation does not only depend on the current program state (which does not contain all necessary information to determine the future evolution of computations). Otherwise stated, transition systems can describe computations that only depend on the current state but not computations which future depends on the computation history to reach the current state. For the sake of generality, we therefore define a semantics (Sect. 2.1) as a set of states, a set of actions and a set of arbitrary traces.
In order to formalize the notion of a program "execution step" which trace semantics is arbitrary we define (Sect. 2.3) the notion of transition system generated by a trace semantics. The transitions are those that can be found along an arbitrary trace of the semantics.
In order to make program correctness proofs, it is often more practical not to reason on the program semantics but on a semantics which is close to it. Such techniques are often used without any justification. To prove their soundness (in Ch. 4 for invariance and Ch. 5 for eventuality), it is necessary to formalize them. We will do it thanks to relations between semantics that are studied in Sect. 2.5 and 2.6.
For example to do the partial correctness of a parallel program, one can ignore the hypothesis that its execution is weakly fair (any process always enabled is ultimately activated). We formalize the relationship between the unfair and fair semantics of this program thanks to a closure of the semantics by reduction to the fair traces (Sect. 2.6.4). In an invariance proof, it s possible to ignore dead code. To prove this, we introduce the notion of closure of a semantics by reduction to reachable states (Sect. 2.6.3). Finally, auxiliary variables are frequently used to prove the partial correctness of parallel programs. The relationship between the semantics of the original program and that of the transformed program (containing the auxiliary variables) can be defined by a reduction of the unobservable actions (to eliminate assignments to auxiliary variables) (Sect. 2.5.4.2) and by conformity with a relation between states (to eliminate the auxiliary variables). When we define a relation between semantics, this induces a relation between transition systems (by considering the relation between the semantics that they generate) which properties are studied.
We observe in Sect. 2.5 that in general, a trace semantics and the transition system that it generates do not provide the same information. Indeed, a trace semantics is in general different from its retract by transitions that is to say the trace semantics generated by the transition system generated by the original trace semantics. In the opposite case, we say that the semantics is closed. This leads us in Sect. 2.6.8 to the characterization of closed semantics (using various operators on trace semantics defined in Sect. 2.6). To sum up, very intuitively, a trace semantics is closed by transitions if and only if it is closed by fusion (Sect. 2.6.5, the future behavior of the execution only depends on the current state that has been reached and not on the way in which this state has been reached), reduced by elimination of the strict prefix traces (Sect. 2.6.6, the stopping of execution in a state only depends on that state) and closed by limits (Sect. 2.6.7, the infinite limits of feasible finite executions are feasible executions).
We state in Sect. 2.7 the problem of the specification of a trace semantics of a program. When the semantics is closed (Sect. 2.7.1), this can easily be done by a transition system (which can itself be defined by induction on the syntax of programs). For a non-closed trace semantics, this is not directly possible. This can always be done indirectly by including summary of the computation history in the states and a controller to monitor the transitions (Sect 2.7.2.2). A non-closed trace semantics can also be specified as a subset of the prefixes of the traces generated by a transition system (Sect. 2.7.2.1). When the semantics is not closed but reduced by elimination of the strict prefix traces, it is sufficient to consider a subset of the traces generated by the transition system (Sect. 2.7.3).
The chapter ends by examples of definition of the semantics of a programming language (Sect. 2.8). The point is to illustrate what was said on the semantics specification methods but mainly to get examples that will be used in the following to illustrate the systematic construction of proof methods. We define the syntax and operational semantics of sequential programs (Sect. 2.8.1, consisting of assignments (ordinary or random), of conditionals and iterations), of asynchronous parallel programs (Sect. 2.8.2, which consist in sequential processes sharing common variables) to which we add in Sect. 2.8.2 the possibility to communicate by rendez-vous by sending and receiving messages on channels (with the possibility to choose between different alternatives as in CSP or ADA) and, in Sect. 2.8.4 the weak fairness hypothesis. Finally, we add in Sect. 2.8.5 the possibility to synchronize processes using semaphores. To show that our definition of semaphores actually corresponds to the initial definition by Dijkstra, we prove some properties of semaphores due to Habermann which are usually supposed to hold without proof. Finally, we provide a liberal semantics of semaphores which can be used to prove invariance properties.
In Ch. 3 we define and briefly illustrate the program properties that we consider in this thesis which are invariance (Sect. 3.2) and eventuality (Sect. 3.3).
Conditional invariance (Sect. 3.2.1) is the most general invariance property that we consider. We say that Ψ is invariant under condition Φ for a trace semantics if and only if for any trace of this semantics and any current state in that trace, the relation Ψ is true between the initial and current state whenever the relation Φ has been true between the initial state and all states before the currents state. We speak of relational invariance (Sect. 3.2.2) when Ψ is identically true and of assertional invariance (Sect. 3.2.3) when Ψ does not depend upon the initial state.
These definitions cover a great number of classical program properties such as partial correctness, absence of runtime errors, non-termination, mutual exclusion, absence of global permanent deadlocks and less classical properties such as precedence properties, for example the current state cannot satisfy Ψ whenever no preceding state did satisfy Ψ.
The eventuality under invariance property (Sect 3.3.1) is the most general inevitability property that we consider. We say that Ψ is inevitable under the invariance f Φ for a trace semantics if and only if for any trace of the semantics there exists a state (called the goal) such that the relation Ψ is true between the initial state and the goal and the relation Φ is true between the initial state and all states reached before the goal. Again we speak of relational eventuality when Φ is identically true and of assertional eventuality if moreover Ψ does not depend upon the initial state.
These definitions also cover a great number of classical program properties such as termination, total correctness, the insurance that a critical section will definitely be entered or that a signal will eventually receive an answer, the absence of starvation of a process, etc.
Other program properties can also boil down to invariance and inevitability on traces, for example by considering suffixes of the program trace semantics or other relations between trace semantics as considered in Ch. 2.
Ch. 4 is devoted to the foundations of the methods for proving invariance properties of sequential, non-deterministic or parallel programs.
We start by studying in Sect. 4.1 the relations between semantics preserving invariance with the idea that to prove an invariance property relative to a program trace semantics we can try to consider a similar property relative to another (usually more simple) semantics.
For example, invariance properties are preserved for semantics conforming up to to relations or functions between state and/or actions (Sect. 4.1.1). They are also preserved after reduction of unobservable states (Sect. 4.1.2). The most important property is that to do an invariance proof for a semantics, it is always sound, and often much simpler, to reason on the generated transition system. Otherwise stated, invariance properties are preserved by retraction of the trace semantics by transitions (Sect. 4.1.3). This proof method is correct but is not in general semantically complete that is to say that there may exist an invariance property that holds for a trace semantics but not for is retraction by transitions. However, the method is semantically complete when the semantics s closed by fusion (Sect. 4.1.3~4) and therefore in particular for the languages considered in Sect. 2.8.
In Sect. 4.2, we study the induction principles that can be used to prove invariance properties of programs. An induction principle describes the essence of a proof method in a concise and abstract way.
As seen in Sect. 4.1, trace semantics are often (but not always) closed. We therefore start by studying this particular case (Sect. 4.2.1). The most well-known method to prove invariance properties of programs is that of Floyd, Naur and Hoare. Starting form an example, we infer the basic induction principle for this method (Sect. 4.2.1.1). Essentially, the induction principle expressed the rather obvious following method: to prove that the reflexive transitive closure t* of a transition relation ∃ a ε A:ta implies an invariant relation Ψ (∀ s, s' ε S, a ε A: t*(s, s') => Ψ(s, s')) it is necessary and sufficient to prove that there exist an invariant I stronger than ψ (∀ s, s' ε S, a ε A: I(s, s') => Ψ(s, s')) which holds for initial states (∀ s ε S: I(s, s)) and stays true for all states reachable from the initial states (∀ s, s' ε S, a ε A: (I(s, s') & ta(s', s'')) => I(s, s'')). In this section we handle relational invariance since the generalization to conditional invariance is trivial (Sect. 4.2.1.1-2).
Then we study the possible variants of this basic induction principle so as to derive all existing proof methods plus some new ones. In order for the study to be systematic, we consider transformations of induction principles (Sect. 43.2.1.2). For a property of the form ([ε(s) & σ(s')] => Ψ(s, s')) relative to a relation between initial and final states, it is possible to restrict the invariant to initial states (Sect. 4.2.1.2.1). Another equally trivial transformation (Sect. 4.2.1.2.2) consists in observing that the verification condition (∀ s, s ε S, a ε A: (∃ s' ε S. I(s, s') & ta(s', s)) => I(s, s)) is equivalent to (∀ s, s ε S, a ε A: I(s, s) => ¬(∃ s' ε S. ta(s, s')& ¬I(s, s')) . Otherwise stated, we can either use a strongest post-condition (like Floyd for the assignment) or else a weakest pre-condition (like Hoare for the assignment). Another transformation (Sect. 4.2.1.2.3) consists in observing that we can reason on inverse relations (t* => Ψ if and only if (t-1)* => Ψ-1)). This allows us to formalize Moris-Wegbreit subgoal induction proof method which therefore consists in applying Floyd's method to the inverse of the program. It is also possible (Sect. 4.2.1.2.4) to replace the invariant I by its negation, which yields contrapositive proof methods by reduction ad absurdum (which are largely ignored in the literature). Finally (Sect. 4.2.1.2.5), when the invariance property to be proved is an assertion (instead of a relation), we can also use an invariant assertion (like in Floyd's method) instead of a relational invariant (as in Manna's proof method).
In Sect. 4.2.1.3 we design the induction principles that we can derive by application of the above transformations, which allows us to find back all classical proof methods and to discover a fez others.
We then show (Sect. 4.2.1.4) that all induction principles are strongly equivalent in that if we have discovered the invariant I which is suitable to do a proof by one method then we can determine the invariant I' that will fit to do the proof by any other induction principle. (By the way this does not prevent a proof by one induction principle to be much easier than by another one). The induction principles are also sound (if the invariant I satisfies the verification conditions then Ψ is invariant) and semantically complete (if Ψ is invariant then we can always find an invariant I satisfying the verification conditions of any of the induction principle (although we may not have syntactic completeness in that the assertion language may not be well-chosen because the invariant I is inexpressible in this language)).
The previous results are generalized to trace semantics which are not closed but nevertheless closed by fusion (Sect. 4.2.2) since in that case, a property is invariant for this semantics if and only if it is invariant for the closure of this semantics by transition.
However this is not true for trace semantics which are not closed by fusion (Sect. 4.2.3).
If this semantics was defined as a subset of the set of prefixes of traces generated by a transition system, it is sound, but not semantically complete, to use the previous induction principles for this transition system. To be complete, we propose an induction principle using auxiliary variables (in the proof not in the program) so as to cumulate histories. This allows the proposed induction principle to take into account the fact that the possible successors of a state do not only depend upon that reachable state but also on the way this state which reached (which we know when cumulating history).
If this semantics is not close by fusion and was defined by conformance with a closed semantics (Sect. 4.2.3.2), we can easily come back to the induction principles that we have studied for closed semantics.
Moreover we show that these new induction principle boil down to the previous ones when the trace semantics is closed by fusion.
Finally (Sect. 4.2.3.3) we show that the two approaches (history summary using auxiliary variables or use of a conforming closed semantics) are strongly equivalent (one proof can be systematically transformed into the other one).
The induction principles as we introduced them as not very easy to use directly in a proof. For example in the verification condition (∀ s, s' ε S, a ε A: (I(s, s') & ta(s', s'')) => I(s, s'')), ta would be a huge formula defining the execution of any computation step of the program. It is therefore preferable to decompose this complex verification condition into a conjunction of simpler verification conditions corresponding for example to each elementary step of the program. This is done in Sect. 4.3 devoted to the systematic design of an invariance proof method from an operational semantics and an induction principle by decomposition of the global invariant into local invariants.
Rather than empirically guessing a proof method for a programming language and then proving a posteriori its soundness and relative completeness, we propose to design the proof method in a systematic way. This consists (Sect. 4.3.1) in first defining the operational semantics by a transition system (Sect. 4.3.1.1), and then in defining the invariance property to be proved (Sect. 4.3.1.2) which allows to chose an suitable induction principle (Sect. 4.3.1.3) among those previously proposed. This induction principle involves a global invariant (on the program states) while a local invariant is usually preferred (e.g. on the memory states attached to program points so that inFloyd's method they can be attached to program points). THe local invariants being chosen (Sect. 4.3.1.4), their semantics mist be defined (Sect. 4.3.1.5) so as to specify the corresponding global invariant and inversely. The design of the proof methods consists in deriving the corresponding local verification conditions. This consists (Sect. 4.3.1.7) in replacing the transition relation by its definition and the global invariant by the local ones in the induction principle that has been chosen and in simplifying the resulting formula so as to obtain elementary verification conditions on local invariants. The derived method is sound by construction. It must then be checked that it is semantically complete (Sect. 4.3.1.8). This verification of completeness can be useless or simplified depending on the nature of the relationship between the global and local invariants. This is why we observe in Sect 4.3.1.6.1 that in general, the set of local invariants is a lattice corresponding to the lattice of global invariants (which are subsets of the set of state pairs). We then study (Sect. 4.3.1.6.2) various possible properties of the correspondences between local and global invariants (monotone correspondences, (semi- or quasi-) Galois correspondences (injective o surjective), complete isomorphisms).
In the next Sect. 4.3.2, we provide examples of systematic design of invariance proof methods, starting by the construction of a proof method of non-termination, absence of runtime errors and global invariance, by reductio ad absurdum, for sequential programs (Sect. 4.3.2.1). Since these methods are not classical, we illustrate them on simple examples.
Then (Sect. 4.3.2.2), we extend the Morris-Wegbreit proof method (so-called "subgoal induction to proof the partial correctness of sequential programs) to parallel programs (in the same way that Owicki-Gris extends Floyd-Naur-Hoare proof method to asynchronous parallel programs) et we generalize it to other invariance properties. We start by considering the partial correctness of sequential programs (Sect. 4.3.2.2.1-4) then global invariance (whereas Morris-Wegbreit though that this was not possible). We then consider the partial correctness of asynchronous parallel programs (Sect. 4.3.2.2.2) where we get back the decomposition of the proof into a sequential proof of each process and a proof of absence of interference between processes. Since this proof method is new, we provide examples of application (such as the asynchronous parallel computation of factorial n!).
We then generalize this proof method to synchronous parallel programs for the proof of absence of permanent global deadlock (Sect. 4.3.2.2.3), the proof of mutual exclusion (Sect. 4.3.2.2.4) and the proof of non-termination (Sect. 4.3.2.2.5).
We then try to explain in Sect. 4.3.2.2.6 with the method of Morris and Wegbreit has not had the same success as Floyd's method. We think that the main reason is well highlighted in the case of parallel programs where the same invariant can be used for the "à la Floyd" methods to prove both the partial correctness, the absence of runtime errors, the absence of deadlocks, mutual exclusion, etc., while this is not the case for the "à la Morris-Wegbreit" methods. To remedy this defect, we propose to use an induction principle combining both forward and backward induction.
We finish be this series of examples by constructing an invariance proof method for communicating sequential processes (Sect. 4.3.2.3). For all the proof methods that we have designed, we have also given a soundness and relative completeness proof.
The proof methods for parallel program as known in the literature (Aschroft, Hoare, Howard, Keller, Lamport, Mazurkievitz, Newton, Owicki-Gries, ...) are often difficult to compare because of the often very different formalisms which are used t present them. The objective of Sect. 4.3.2.4 is to show that they all derive from the same induction principle (underlying Floyd's method) and that they only differ by the way the global invariant used in the induction principle is decomposed into local invariants attached to program points.
For example, the method of Ashcroft and that of Keller consist in using a single global invariant (Sect. 4.3.2.4.1). This was the first generalization of Floyd's method to parallel programs but it has the default to have a single global verification condition which is not decomposed into more elementary local verification conditions.
Inversely, the method of Ashcroft-Manna consists in using a local invariant attached to each control state (Sect. 4.3.2.4.3). In this case, the decomposition is too fine, which has the consequence that the number of verification conditions is much too high.
A first compromise in Owicki-Gries proof method consists in using a local invariant on variables associated to each program control point (and no longer to each state) (Sect. 4.3.2.4.3). But this method is semantically incomplete.
This can be remedied by following Newton and Lamport who use local invariants on the state of control and on the variables attached to each program control point (Sect. 4.3.2.4.4).
We can also follow Owicki-Gries who proposed to used local invariants on the program variables as well as on auxiliary variables attached to the program control points (Sect. 4.3.2.4.5). We show that the method is sound and semantically complete (by defining the auxiliary semantics, which can always be used to do the proof, up to a reduction of the unobservable states and up to a function of the states. In this auxiliary semantics, the control states are simply simulated by variables, which shows that the auxiliary variables are only used in Owicki-Gries method to simulate the control state of which the local invariants are independent).
With these decompositions, the number of verification conditions is proportional to the product of the lengths of the parallel program processes whereas, n practice, one would like the number of verification conditions to grow linearly with the size of the program. This is the case of a method proposed by Lamport which consists in using local invariants on the control and variables associated to each process of the parallel program.
It is finally possible ti use a redundant information (as is the case in the methods proposed by Hoare, Howard, ...) under the form of a global invariant and of local invariants attached to various program points (Sect. 4.3.2.4.7).
This profusion of proof methods leads us a classify them according to the underlying induction principle and according to the coarseness of the decomposition of the global invariant into local invariants (Sec. 4.3.2.4.8).
To conclude this section, we think that the examples that we have given show that the choice of the coarseness/precision of the decomposition of the global invariant into local invariants should not be fixed once for all in a proof method. It would be preferable to chose this decomposition according to the problem to be solved. The formalization of the invariance proof methods that we have proposed allows us to do this without difficulty.
We finish this chapter on invariance proof methods by Sect. 4.3.2.5 dealing with the static analysis of programs. We do it because this problem (which, let us recall it, consists in automatically and statically inferring invariants for a program) has motivated the the work that we present here. We mainly do it to show that the results obtained for sequential programs can be easily generalized to parallel programs. The presentation will be very short. We simply recall how a static analysis can be done "forward" (Sect. 4.3.2.5.1, to determine a superset of the states reachable from initial states), how a static analysis can be done "backward" (Sect. 4.3.2.5.2, to determine a superset of the set of ascendants of final states) and how a combined static analysis can be done "forward-backward" (Sect. 4.3.2.5.3, to determine a superset of the set of descendants of the initial states which are ascendants of final states). Since the formalism that we use is very general and since it includes parallel programs we will simply provide a few examples to demonstrate the application of static analysis methods to this type of programs.
Ch. 5 deals with eventuality proof methods for sequential and parallel programs.
A number of results obtained in the previous chapter (such as the transformation of induction principles, the decomposition of a global invariant into local invariants,...) can equally will be applied in this chapter (may be with necessary slight adaptations). To avoid repetitions, we will not reconsider the same idea in this chapiter even though they are applicable.
This chapter includes two important paragraphs, Sect. 5.2 handles "À la Floyd" induction principle and Sect. 5.3 handles "À la Burstall" induction principles, In fact we could have made a different presentation by introducing Sect. 5.2 in a few sentences as a particular case of Sect. 5.3. However we choose to go from the particular (Sect. 5.2) to the general (Sect. 5.3) in order to follow the historical evolution and mainly to grade the difficulties. To avoid repetitions, we introduce in Sect. 5.2 a number of results (such as the induction principles for the non-closed semantics, ...) which are not repeated in Sect. 5.3 since their generalization does not appear to present any difficulty once the idea has been illustrated in Sect. 5.2.
We start our study of the eventuality proof methods by that of relations between semantics that preserve eventuality (Sect. 5.1)> Unfortunately, the positive results are much less numerous than in the case of invariance. Without trying to be exhaustive, we show (Sect. 5.1.1) that eventuality properties are preserved by inclusion of semantics (but in one direction only since e.g. it is not always possible to prove an eventuality property for a synchronous parallel program by reasoning on the liberal semantics of semaphores) and that (Sect. 5.1.2) the eventuality properties are preserved for semantics that coincide up to relations between states and actions (in both directions, under certain restricting conditions).
In Sect. 5.2, we formalize eventuality proofs by induction principles generalizing Floyd's method.
We first recall in Sect. 5.2.1 the principle of Floyd's proof method (so-called of invariant assertions and well-founded order) to prove the total correctness of sequential programs.
This allows us extract the basic induction principle to prove eventuality properties for closed semantics (Sect. 5.2.2).
We then study a series of induction principles which are equivalent to the basic induction principle (Sect. 5.2.3) that reflect some of the possible variants of Floyd's method. For example, it is not necessary to associate a termination function to all program control points but only to cut-points of loops. The use of well-orders is not mandatory and well-founded relations are sufficient and sometimes easier to use. The termination function can be replaced by an auxiliary variable (in the proof but not necessarily appearing in the program) that strictly decreases at each program computation step. This auxiliary variable can always we chosen to be an ordinal, etc.
We then consider the problem of the soundness and of the semantic completeness of the previous induction principles à la Floyd.
We observe in Sect. 5.2.5 that is the inevitability property is a relation between initial and final states, the termination function must, in general, be applied not only to the current state but also to the initial state (a fact that many reference books ignore so that they introduce a semantically incomplete method).
It is also interesting to characterize the well-founded relations (or equivalently the ordinals) which are necessary to make eventuality proofs based on the induction principles generalizing the basic principle underlying Floyd's method (Sect. 5.2.6). To do so, we consider that the non-determinism of a trace semantics is m-bounded, if the cardinal of the set of successors of any state for the transition relation generated by this trace semantics is strictly less that m. In particular the non-determinism is finite (Dijkstra says "bounded"0 if any state has a finite number of possible successors. We show that, for a closed semantics, the non-determinism of which is m-bounded, it is always possible to make inevitability proofs with well-founded relations which order is less that m+ (where m+ = ω if m+ < ω, m+ = m when m is a regular cardinal else m+ is the smallest cardinal strictly greater than m). This limit is strict when m is regular. As a particular case, we derive that the Knuth-Luckham-Suzuki method (which consists in using a counter strictly incremented at each loop iteration and which value is bounded) is not semantically complete when the non-determinism is not finite (and so cannot be generalized to the case of fair parallel programs).
Sect. 5.2.7 deals with the decomposition of the verification conditions. The general case was studied in Sect. 4.3, so we just illustrate a few possible decompositions (in order to show that Lamport and Owicki-Gries proof methods initially designed for partial correctness can be extended to total correctness proofs).
Having only considered closed semantics up to now, the case of eventuality proof methods for fait parallel programs was excluded. Therefore, we study in Sect. 5.2.8 the "à la Floyd" induction principles to prove eventuality properties of non-closed semantics.
As was the case for invariance, we can define the non-closed semantics y correspondence with a closed semantics up to a function of the states (Sect. 5.2.8.1). In these conditions, any of the induction principles introduced for closed semantics can be used. This amounts, e.g. for a fair parallel program, to reason on a transformed program including an execution controller/monitor ensuring fairness.
Another approach (Sect. 5.2.8.2) can be used when the non-closed trace semantics is specified by a subset of the prefixes of the traces generated by a transition system. It consists in accumulating the computation history in an auxiliary variable. This allows, when the semantics is not closed by limits, ne to require the termination function to decrease at each computation step but only at cut-points which need not be determined statically as was the case in Floyd's method but dynamically, depending on the computation history. In particular, we obtain the Pnueli-Lehmann-Stavi method to prove the total correctness of weakly fair parallel programs, which essentially consists in applying Floyd's method but with the possibility that the termination function does not strictly decrease while a process remains enabled while never being activated . Moreover, when the trace semantics is not reduced by elimination of the strict trace prefixes, the computation history is used to ensure that the goal is reached for finite traces before the end of the trace (which may not be a state without successor). Finally, when the semantics is not closed by fusion, the invariant must hold for all states which can be reached for all states that can be reached by following the prefix of a trace where the goal is never reached but not necessarily for all prefixes obtained by successive transitions. Here again, the accumulation of the history in an auxiliary variable is useful.
Finally, we show in Sect. 5.2.8.3 that the two approaches (using an auxiliary semantics including an execution controller/monitor or else the use of history variables to cumulate the computation history) are equivalent.
In Sect. 5.3.1, we introduced Burstall intermittent assertions proof method by means of examples from which we derive a basic induction principle formalizing this proof method is a very concise way. We show that this induction principle is sound. The semantic completeness issue is more complex. Using transfinite induction (rather than finite since the induction principles generalizes Burstall's method to infinite non-determinism) we show that this induction principle is semantically complete under a sufficient condition (which is not necessary) on the semantics and the inevitability property. This condition expressed that a state cannot be a goal on a trace and belong to a prefix of another trace along which the goal has not been reached. This condition is obviously satisfied in the case of Burstall who considers deterministic programs and also for generalizations to non-deterministic programs (Pnueli, Apt-Delporte,,,,) where the considered inevitability properties are unary and do not depend upon initial states.
When considering unary inevitability properties , the relations between the initial and final values of program variables can only be expressed by considering a transformed program in which the initial values of variables are assigned to auxiliary variables. Besides the program transformation without fundamental motivation, the use of auxiliary variables is in a sense too flexible because they can be used to relate arbitrary intermediate states of a computation and even to cumulate the full history of computation. Such a freedom in the use of auxiliary variable is not in the spirit of Burstall's method and of the examples given by Manna and Waldinger where the lemmata proved by induction on the data structures are always of the form:
This conjecture leads us in Sect. 5.2.3 to generalize the intermittent assertions proof method of Burstall using transfinite induction (to handle unbounded non-determinism) and ternary intermittent assertions (so as to express lemmata of the more general form
" if sometime Φ(x1,...,xn,X1,...,Xn) & X1=x1 & ... & Xn=xn at l then
sometime Ψ(x1,...,xn,x1,...,xn,X1,...,Xn) at l'" " where x1,...,xn (respectively x1,...,xn) denote the values of the program variables at the program entry point (respectively at program point l). We prove that this induction principle is sound and semantically complete.
From this induction principle, we derive in Sect. 5.3.3 a whole series of induction principles which are more and more abstract and concise. For example, it is interesting to consider a transfinite and no longer finite number of intermittent assertions (that we can finitely represent using auxiliary variables). This extends Burstall method so as to include Floyd's method and to use binary and no longer ternary intermittent assertions (formally using a different lemma for each inital state). Among these induction principles, there is one which formalizes Schwarz idea that Burstall method consists in proving theorems by mathematical induction from axioms specifying the computational effect of the program elementary commands. The most abstract induction principles provide a better understanding of Burstall's method (for example, we prove that the "symbolic execution" and the "induction on data" can be understood in a unified way and reduced to an induction on computations. These successive generalizations introduce more flexibility in the proof writing but no additional expressive power since we show that all considered are sound and semantically complete hence equivalent. Since the most abstract induction principles may appear to be very far form Burstall's method we provide a few examples to prove the contrary.
The "À la Floyd" induction principle is by induction along execution traces while the "À la Burstall" induction principle include a combination of an induction along part of execution traces (relqted to the "symbolic execution" of Burstall) and recursion (related to the "little induction" on data of Burstall). The "À la Floyd" induction principle corresponds to the particular case of the "À la Burstall" induction principle where recursion is not used. An immediate consequence is that the "À la Burstall" induction principle is semantically complete since we previously proved that the is the case of the "À la Floyd" induction principle. This remarks also explain why Burstall method is better adapted than Floyd's method to prove the total correctness of iterative programs obtained by recursion elimination (the reason being that ii is possible to preserve recursion in the proof). More important is the fact that the "À la Burstall" induction principle offers more possibilities to decompose the proof of an inevitability theorem into proofs of simpler independent lemmatas, which is impossible with Floyd's method requiring a global proof (Sect. 5.3.5).
The semantic completeness argument of the "À la Burstall" induction principle is not plainly satisfactory since the allowed style of the proofs is fixed. The users of Burstall's method need a stronger completeness result since they would like to know if the lemmata that they intend to use in their proofs can always be freely chosen. A positive answer is given in Sect. 5.3.4 (with the necessary and sufficient condition tjat each lemma must express an inevitability property for the program but also relative to all other lemmata that are used in the proof).
The comparison of Floyd's and Burstall's proof methods (Manna-Waldinger, Gries, ...) was somewhat polemical, some asserting that there are programs having a "natural" proof by Burstall's method and not with Floyd's method, the others working enough on Floyd's method until putting it in a forming appearing as simple. (Most of the provided examples (such as the iterative version of Ackermann function) were obtained by elimination of recursion and we provide an example in Sect. 5.4-1 which is simple, looks convincing and is not of this form). As a contribution to this debate, we prove in Sect. 5.4 that any proof by one method can be systematically rewritten as a proof by the other method. The proof is somewhat long and technical but intuitively the transformation between the two proofs is very similar in one direction to recursion elimination in programs and in the other direction to the recursive presentation of iterative programs, (we do not pretend that these transformations preserve the "naturalness" of the proofs).
Having shown that Floyd's method is a particular case of Burstall's method (after the adequate generalizations that we have done), it remains nevertheless that the classical presentations of the proofs by invariant assertions on one hand and intermittent assertions on the other hand are dissimilar enough that it is difficult to present these two methods in a uniform framework. This is why we introduce in Sect. 5.5 the notion of proof chart.
The idea of presenting program proofs graphically by acyclic diagrams was introduced by Lamport and developed by Owicki-Lamport and Manna-Pnueli. Yet, these methods where not semantically complete because of a certain number of restrictions, mainly the impossibility of doing infinite inductions. Our formalization is more general since it consists in introducing proof charts which are well-structures, may include cycles and may be recursively used for proofs by induction on data. After having defined the notion of proof chart (Sect. 5.5.1), we proof the soundness and completeness of the method y proving that is corresponds to the use of an "À la Burstall" induction principle (Sect. 5.5.2). We then provide a few examples of proof presentations by charts (Sect. 5.5.3) to show that "À la Floyd" proofs can be presented very naturally by proof charts and also to show that proof charts are very useful to prove eventuality properties of asynchronous parallel programs. Finally, the ideas developed in Sect. 5.2 about the eventuality proofs for non-closed semantics are directly applicable. We show it simply, by examples extending the inevitability proofs by proof charts to the case of weakly fair parallel programs and then to the case of synchronous programs.
Chapter 6 is a brief conclusion. The references are provided at the end of this chapter.
\bibitem{CousotR-TheseEtat-1985}
R. Cousot.
\newblock Fon\-de\-ments des m{\'e}\-tho\-des de preu\-ve d'in\-va\-rian\-ce et de
fa\-ta\-li\-t{\'e} de pro\-gramm\-es pa\-ral\-l{\`e}\-les (in {F}rench).
\newblock Th{\`e}\-se d'{{\'E}}tat {\`e}s sci\-en\-ces ma\-th{\'e}\-ma\-ti\-ques,
Ins\-ti\-tut Na\-tio\-nal Po\-ly\-tech\-ni\-que de Lor\-rai\-ne, Nan\-cy,
Fran\-ce, 15 November 1985.
@phdThesis{CousotR-TheseEtat-1985,
author = {Cousot, R{.}},
title = {Fon\-de\-ments des m{\'e}\-tho\-des de preu\-ve d'in\-va\-rian\-ce et de
fa\-ta\-li\-t{\'e} de pro\-gramm\-es pa\-ral\-l{\`e}\-les (in {F}rench),
type = {Th{\`e}\-se d'{{\'E}}tat {\`e}s sci\-en\-ces
ma\-th{\'e}\-ma\-ti\-ques},
school = {Ins\-ti\-tut Na\-tio\-nal Po\-ly\-tech\-ni\-que de Lor\-rai\-ne},
address = {Nan\-cy, Fran\-ce},
month = {21 November},
year = 1985,
}