by specifying pre- and post-conditions. Preconditions and post-conditions are
predicates such that if the precondition correctly characterizes a program’s state
on entry to the function, the post-condition is established upon exiting. An
invariant is another important concept from this early work on formal methods.