lAt one level of abstraction, a program is a relation between input and output
values.
lIt is common to express this relation as a pair of assertions about the state of a program:
lThe input assertion specifies what is must be true at the start in order for the
program to be applicable.
lThe output
assertion specifies what will be true at
the end.
lSuch assertions are predicates on program state.