Slide 10.3: Applications of Hoare logic (cont.)

Slide 10.2: Applications of Hoare logic
Slide 10.4: The weakest precondition wp
Home

Applications of Hoare Logic (Cont.)

Precondition/postcondition pairs can be useful in specifying the expected behavior of programs—the programmer simply writes down the conditions he or she expects to be true at each step in a program. For example, a program that sorts the array a[1] … a[n] could be specified as follows:

   {n ≥ 1 and for all i, 1 ≤ i ≤ n, a[i] = A[i]}
   sort-program
   {sorted( a ) and permutation( a, A )}

The assertions are as follows:

The assertion sorted(a) means the elements of a are sorted.
The assertion permutation( a, A ) means the elements of a are the same, except for order, as the original elements of the array A.

Such preconditions and postconditions are often capable of being tested for validity during execution of the program, as a kind of error checking. For example, the C language also has a rudimentary but useful macro library for checking simple assertions: assert.h. Using this library and the macro assert allows programs to be terminated with an error message on assertion failure, which can be a useful debugging feature:

 #include  <assert.h>
 #include  <stdio.h>
 #include  <stdlib.h>
 
 int main( int arc, char* argv[ ] ) {
   int x = 0; 
   int y = ; 
 
   for ( x = 0;  x < 20;  x++ ) {
     printf( "\nx = %d   y = %d", x, y ); 
     assert( x < y ); 
   }
 }

This program keeps printing the values of x and y. When x ≥ y, the program halts and an error message is printed.