Example I of Program Correctness


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: 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}