Content deleted Content added
Merge wlp into this article |
|||
Line 6:
This gives a predicate that is a copy of ''R'' with the value of ''x'' replaced by ''E''.
An important variant of the weakest precondition is the '''weakest liberal precondition''' <math>wlp(S, R)</math>, which yields the weakest condition under which ''S'' either does not terminate or establishes ''R''. It therefore differs from ''wp'' in not guaranteeing termination.
An example of a valid calculation of ''wp'' for assignments with integer valued variables ''x'' and ''y'' is:
Line 28 ⟶ 30:
* [[Ralph-Johan Back]] and [[Joakim von Wright]], ''Refinement Calculus: A Systematic Introduction'', 1st edition, 1998. ISBN 0-387-98417-8.
* [[Marcello M. Bonsangue]] and [[Joost N. Kok]], [http://dx.doi.org/10.1007/BF01213603 ''The weakest precondition calculus: Recursion and duality''], ''[[Formal Aspects of Computing]]'', '''6'''(6):788–800, November 1994. [[Digital object identifier|DOI]] 10.1007/BF01213603.
* [[Edsger W. Dijkstra]], ''Guarded commands, nondeterminacy and formal derivation of program''. ''[[Communications of the ACM]]'', 18(8):453–457, August 1975. [http://doi.acm.org/10.1145/360933.360975]
* [[Edsger W. Dijkstra]]. ''A Discipline of Programming''. ISBN 0-613-92411-8. — A systematic introduction to a version of the guarded command language with many worked examples
* [[Edsger W. Dijkstra]] and [[Carel S. Scholten]]. ''Predicate Calculus and Program Semantics''. Springer-Verlag 1990 ISBN 0-387-96957-8 — A more abstract, formal and definitive treatment
* [[David Gries]]. ''The Science of Programming''. Springer-Verlag 1981 ISBN 0-387-96480-0
* [[Leslie Lamport]], "''win'' and ''sin'': Predicate Transformers for Concurrency". ''[[Association for Computing Machinery|ACM]] Transactions on Programming Languages and Systems'', 12(3), July 1990. [http://research.microsoft.com/users/lamport/pubs/pubs.html#lamport-win]
{{formalmethods-stub}}
[[Category:Formal methods]]
| |||