weakest precondition
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.
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.
More From encyclopedia.com
Axiomatic Semantics , axiomatic •achromatic, acrobatic, Adriatic, aerobatic, anagrammatic, aquatic, aristocratic, aromatic, Asiatic, asthmatic, athematic, attic, autocrati… Computer Program , pro·gram / ˈprōˌgram; -grəm/ (Brit. pro·gramme) • n. 1. a planned series of future events, items, or performances: a weekly program of films the prog… Tsr , TSR Short for terminate and stay resident program. A type of program normally found on microcomputer systems. After the program has been loaded into… Food Stamps , FOOD STAMP PROGRAM. The food stamp program originated in federal efforts to combat overproduction during the Great Depression by raising the consumpt… Ada , Ada Trademark A programming language developed at the behest of the US Department of Defense for use in real-time systems containing embedded compute… Fp , FP A notation for functional programming proposed by J. W. Backus in 1978. Backus propounded a general functional style of programming, and developed…
You Might Also Like
NEARBY TERMS
weakest precondition