Slide 11.6: Example I of program correctness

Slide 11.5: Proofs of program correctness
Slide 11.7: Example I of program correctness (cont.)
Home

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:

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}