Program Specification
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.