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 means
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.
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.
Firstly, we determine the labels of C. Let
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:
, 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.
As a corollary, we can state the semantical soundness and completeness of the Floyd–Naur stepwise method.
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 .