weakest precondition

views updated

weakest precondition For some given program statement S and some postcondition R there is a (possibly empty) set of program states such that if execution of S is initiated from one of these states then S is guaranteed to terminate in a state for which R is true. The weakest precondition of S with respect to R, normally written wp (S,R)

is a predicate that characterizes this set of states. Use of the adjective weakest explicitly indicates that the predicate must characterize all states that guarantee termination of S in a state for which R is true.

The term was introduced by Dijkstra in 1975 in conjunction with a calculus for the derivation of programs; this provides for development of a program to be guided by the simultaneous development of a total correctness proof for the program. See program correctness proof, predicate transformer.