Axiomatic semantics: Axiomatizing programming languages

pp 309-310
9.4.1 Assertions
9.4.2 Preconditions and postconditions

These ideas lie at the basis of a theory of software construction
which has been termed *programming by contract*.

Defined this way, program correctness is only a *relative* concept:
there is no such thing as an intrinsically correct or intrinsically
incorrect program. We may only talk about a program being correct or
incorrect with respect to a certain specification, given by a
precondition and a postcondition.

9.4.3 Partial and total correctness

pp 312-313, 9.5.1 Assertions and boolean expressions

[...] a boolean expression may be taken as representing an assertion
[...] -the assertion satisfied by those states in which the boolean
expression has value true.

Does this indicate a one-to-one correspondence between assertions and
boolean expressions? there is actually two questions:

1. Given an arbitrary boolean expression of the programming language,
   can we always associate an assertion with it?
2. Can any assertion of interest for the axiomatic theory of a
   programming language be expressed as a boolean expression?

[...] this should not lead us to confuse assertions with boolean
expressions; and there are both theoretical and practical reasons for
keeping the two notions distinct.

On the theoretical side, assertions and boolean expressions belong to
different worlds:
. Boolean expressions appear *in* programs: they belong to the
  programming language.
. Assertions express properties *about* programs: they belong to the
  formulae of the axiomatic theory.

On the practical side, [...] all common programming languages [...]
yield a negative answer to both question 1 and 2 above.