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

Proof.() iff . This meansLet

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

Cwith and .() Assume for some . Then . Moreover, by induction on

nwe 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 forCwith 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 programCcomputing the largest common multiplier ofaandb.;

;

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

Pand 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 parametersXandYof 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

Ptrue. Then:

By this, we can conclude that define local invariants for program

C. Moreover, if we defineias

then we have

and, if , then . In addition, . hence, we can conclude that

iis a global invariant forC.

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:

, if is skip

, where is and for any

, if

*L*begins with a while- or conditional instruction with condition*B*, and is the next label when*B*is true, if

*L*begins with a while- or conditional instruction with condition*B*, and is the next label when*B*is false

We assert the following theorem without proof.

Theorem 26.LetCbe a program, assume . Let define local invariants forC. Then holds true, if is a local invariance condition forC, 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 forC, 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 forC, , . 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].