Content deleted Content added
m Disambiguating links to Coq (link changed to Coq (software); link changed to Coq (software); link changed to Coq (software)) using DisamAssist. |
No edit summary |
||
Line 6:
== Weakest preconditions ==
=== Definition ===
For a statement ''S'' and a [[postcondition]] ''R'', a '''weakest precondition''' is a predicate ''Q'' such that for any [[precondition]] {{mvar|P}}, <math>\{ P \} S \{ R \}</math> if and only if <math> P \Rightarrow Q </math>. In other words, it is the "loosest" or least restrictive requirement needed to guarantee that ''R'' holds after ''S''. Uniqueness follows easily from the definition: If both ''Q'' and ''Q' '' are weakest preconditions, then by the definition <math>\{ Q' \} S \{ R \}</math> so <math> Q' \Rightarrow Q </math> and <math>\{ Q \} S \{ R \}</math> so <math> Q \Rightarrow Q' </math>, and thus <math> Q=Q' </math>. We often use <math>wp(S, R)</math> to denote the weakest precondition for statement ''S'' with
=== Conventions ===
| |||