Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:assert_and_error_conditions [2010/03/08 13:49] vkuncak |
sav08:assert_and_error_conditions [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 28: | Line 28: | ||
| We assume that the desired properties $P$ satisfy | We assume that the desired properties $P$ satisfy | ||
| - | \[ | + | \begin{equation*} |
| \models P \rightarrow OK | \models P \rightarrow OK | ||
| - | \] | + | \end{equation*} |
| ===== Desired Rules for Weakest Preconditions ===== | ===== Desired Rules for Weakest Preconditions ===== | ||
| For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold: | For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold: | ||
| - | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
| \models wp(c,Q) \rightarrow OK \\ | \models wp(c,Q) \rightarrow OK \\ | ||
| wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\ | wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\ | ||
| Line 43: | Line 43: | ||
| wp(assume(F),Q) = (OK \land (F \rightarrow Q)) \\ | wp(assume(F),Q) = (OK \land (F \rightarrow Q)) \\ | ||
| wp(assert(F),Q) = (F \land Q) | wp(assert(F),Q) = (F \land Q) | ||
| - | \end{array}\] | + | \end{array}\end{equation*} |
| We assume above that $x$ is not the //error// variable. | We assume above that $x$ is not the //error// variable. | ||