The stepwise Floyd–Naur method

The stepwise Floyd–Naur method is considered as an induction principle checking the validity of the property through the subsequent parts of the program. We can identify an invariant property of the program, which is a property remaining true during the course of the execution of the program. The invariance of that property can be checked by verifying local invariance conditions: if the property holds at a point of the execution then it will hold at the next point, too. It only remains to check that if we start from the precondition , then the set of states at the termination of the program is contained in the postcondition . We start with the necessary terminology.

We call a global verification condition, or global invariant, if the following holds:

We can assert the following claim

Lemma 23. iff there exists an i such that .

Proof. () iff . This means

Let

Trivially and , by Equation 1.1. We have to prove . But this is immediate from the definition of . We can conclude that is a global verification condition for C with and .

() Assume for some . Then . Moreover, by induction on n we can see that , thus . Hence, if ,

Hence the partial correctness with respect to and indeed holds.

Remark 24. We state without proof that, if , then is the strongest global verification condition for C with and . In other words, if , then .

Instead of global invariance we consider local invariants at certain program points in practice. In fact, the designations of program points mimic program executions. Local invariants attached to program points can be corresponded to global invariants in a bijective way. A label is a program: intuitively, we mark every program point with a label, which is the part of the original program yet to be executed. We denote the set of labels of C by . Let be a global invariant, then is a local invariant, where and

Conversely, let define local invariants, then is a global invariant, where for the function

where is the endlabel symbol.

Example 25. Consider the program C computing the largest common multiplier of a and b.

;

;

while do

    if then

        

    else

        

    fi

od

Firstly, we determine the labels of C. Let

Then

Assign set of states to the labels in the following way. As an abuse of notation, we omit the distinction between a first order formula P and the value of the formula , which denotes the set of such that in our fixed interpretation . To make the relation of the assertions assigned to labels more discernible, we indicate the possible parameters X and Y of every when writing down .

If we assign assertion to label , we find that the assertions satisfy the following local verification conditions. Let us define iff , where denotes the set of states which make P true. Then:

By this, we can conclude that define local invariants for program C. Moreover, if we define i as

then we have

and, if , then . In addition, . hence, we can conclude that i is a global invariant for C.

In order to state the next theorem, we define informally the notion of local invariance condition. Let C be a program, assume , We say that is a local invariance condition for C, and , if the following hold: let , assume is the label of the next program point and is the command to be executed next. Then:

We assert the following theorem without proof.

Theorem 26. Let C be a program, assume . Let define local invariants for C. Then holds true, if is a local invariance condition for C, and .

As a corollary, we can state the semantical soundness and completeness of the Floyd–Naur stepwise method.

Theorem 27. (semantical soundness and completeness of the stepwise Floyd–Naur method) iff there exists a local verification condition for C, and .

Proof. We give a sketch of the proof. First of all, we should notice that the if-case is the statement of the previous theorem. For the other direction we can observe that if , then is a global verification condition for C, , . Then it is not hard to check that defined as

satisfies the local invariance condition. By Theorem 26, the result follows.

We remark that there also exists a compositional presentation of the Floyd–Naur method, which is equivalent in strength to the stepwise method illustrated above. We omit the detailed description of the compositional method, the interested reader is referred to [3].