Weakest liberal precondition
From Wikipedia, the free encyclopedia
A weakest liberal precondition (wlp) is an extension of the concept of weakest precondition by E. W. Dijkstra for proofs about computer programs. While wp guarantees termination wlp does not.
[edit] References
- Marcello M. Bonsangue and Joost N. Kok, The weakest precondition calculus: Recursion and duality, Formal Aspects of Computing, 6(6):788–800, November 1994. DOI 10.1007/BF01213603.