Partial correctness of while-programs

In this section we lay the foundations for the systematic verification of programs. To this extent, we augment the expressibility of our language a little. Firstly, we add variables representing natural numbers to our arithmetic constructions. Thus an arithmetical expression will look like as follows

where the new member is i, a variable denoting an integer value or a natural number. Next we extend Boolean expressions to be appropriate for making more complex statements about natural numbers or integers. We obtain the set of first order formulas or first order expressions in this way.

We define free and bound variables, substitution, renaming as usual. As to the abbreviation of formulas, we stipulate that the quantifiers should be the first in priority, which is followed by negation. Conjunction and disjunction have equal strength, they come after negation but precede implication and equivalence, which is the weakest of all operators. As mentioned before, an execution of a while program can be considered as a state transformation: we start from one state and through consecutive steps, if the program halts, we obtain the final state where no more command can be executed. This approach manifests itself most obviously in the definition of the denotational semantics of programs. Therefore, we can describe the execution of programs by a pair of sets of states.

Definition 22. Let , . Then the pair is called a specification. We say that the program C is correct with respect to the specification if, for every , if there is an such that , then . More formally, C is correct with respect to the specification , if

We use the notation for the value of the predicate .