This chapter shows how, by having syntax, semantics, preconditions, and postconditions all in the same formal and executable language (OBJ), we can (relatively!) easily do formal proofs of correctness, without annoying problems with Hoare semantics like the following: Consider the Hoare triple
{ a >= 0 & b >= 0 } S { z = a * b }
which seems to intend to specify that a fragment S of code should
multiply a and b. However, the following
S satisfies the above Hoare triple
z := 0 ; a := 0even though it does no multiplication at all!
This is an example of what can happen when different kinds of variables are treated as being the same. It is a problem with variables in the usual formulation (as in chapter 3 of Sethi) of Hoare semantics; it is not at all a problem with the semantics of programs as such. The solution is to introduce ghost variables, also called specification constants, and use them in both the pre- and the post- condition.
Note that in the framework of Algebraic Semantics, program variables
are constants in the syntax of the programming language (as they
should be), so that it does not even make sense to make assertions of the form
'X >= 0 ; it is necessary to include a store to get a value, as
in
S [['X]] >= 0 .However, one can still write specs that are statisfied by bogus programs, if one is not careful about quantification, as in
S[['X]] >= 0 and S[['Y]] >= 0 imply S;P[['Z]] = S;P[['X]] * S;P[['Y]] .Instead, one should write specifications like
(forall a,b >= 0) S[['X]] = a and S[['Y]] = b imply S;P[['Z]] = a * b .
There is a typo on page 84; the equation at the top of the page should be
(s ; absx [[`Z]]) is abs(x)