The axiomatic semantics of the previous slides will be used to prove properties of programs written in the sample language.
A correct program is one that meets its specification.
In other words, a program is correct with respect to a precondition and a postcondition provided that, if the program is started with assumptions that make the precondition true, the resulting values make the postcondition true when the program terminates.
Again, a specification for a program C can be written as
{P} C {Q}
As an example, we gave the following specification for a program that sorts the array a[1] … a[n]:
{n ≥ 1 and for all i, 1 ≤ i ≤ n, a[i] = A[i]}
sort-program
{sorted( a ) and permutation( a, A )}
Two easier examples of specifications for programs that can be written in the sample language will be proved for their correctness next.
Recall that C satisfies a specification {P}C{Q} provided P → wp(C, Q).
Thus, to prove that C satisfies a specification we need two steps:
- First, we must compute
wp(C,Q) from the axiomatic semantics and general properties of wp.
- Second, we must show that
P → wp(C,Q).
We claim that the program, which swaps the value of x and y, is correct:
{x = X and y = Y}
t := x; x := y; y := t;
{x = Y and y = X}