weakest precondition

Show Summary Details

Quick Reference

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.

wp (S,R)

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.

Subjects: Computing.

Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.