Differences
This shows you the differences between two versions of the page.
sav08:assert_and_error_conditions [2009/03/12 16:12] vkuncak |
sav08:assert_and_error_conditions [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ===== Asserts and errors for nice wp definition ===== | ||
- | We used assert(F) to express conditions that should hold. | ||
- | |||
- | Can we give executation semantics to assert? | ||
- | |||
- | assert(F) = irrecoverable error if $F$ is false, terminates execution. | ||
- | |||
- | wp computes conditions sufficient for errors not to happen. | ||
- | |||
- | Postconditions are just asserts at the end of the program. | ||
- | |||
- | How to build a system with relations where at the same time | ||
- | wp(assert(F),Q) = (F & Q) | ||
- | wp(assume(F),Q) = (F --> Q) | ||
- | |||
- | Then | ||
- | wp(assert(false); assume(false),Q) = false | ||
- | wp(assume(false); assert(false),Q) = true | ||
- | so cannot have $\mbox{assume(false)} = \emptyset$ any more. | ||
- | |||
- | ===== Error Variable and Good States ===== | ||
- | |||
- | Introduce variable "error". Good states are states where this variable has value zero. We write OK for the formula error=0. | ||
- | |||
- | We assume that the desired properties $P$ satisfy | ||
- | \[ | ||
- | \models P \rightarrow OK | ||
- | \] | ||
- | |||
- | ===== Desired Rules for Weakest Preconditions ===== | ||
- | |||
- | For all $Q$ such that $\models Q \rightarrow OK$, we would like the following to hold: | ||
- | \[\begin{array}{l} | ||
- | \models wp(c,Q) \rightarrow OK \\ | ||
- | wp(c1 [] c2,Q) = wp(c1,Q) \land wp(c2,Q) \\ | ||
- | wp(c1 ; c2,Q) = wp(c1,wp(c2,Q)) \\ | ||
- | wp(havoc(x),Q) = \forall x.Q \\ | ||
- | wp(x=e,Q) = Q[x:=e] \\ | ||
- | wp(assume(F),Q) = (OK \land (F \rightarrow Q)) \\ | ||
- | wp(assert(F),Q) = (F \land Q) | ||
- | \end{array}\] | ||
- | |||
- | We assume above that $x$ is not the //error// variable. | ||
- | |||
- | Note: we wrote $OK \land ...$ in the weakest precondition of assume, but usually $OK$ is implicit and we do not write it. We do not need it in other cases because it follows that right hand side implies $OK$. | ||
- | |||
- | |||
- | ===== Relational Semantics that Fulfills These Rules ===== | ||
- | |||
- | Let OK denote s(error)=0 and OK' denote s'(error)=0. We define: | ||
- | \begin{eqnarray*} | ||
- | R_c(\mbox{havoc(x)}) &=& \{(s,s') \mid OK \rightarrow (OK' \land s'(y)=s(y)) \} \\ | ||
- | R_c(\mbox{assert}\ F}) &=& \{(s,s') \mid (OK \land F(s)) \rightarrow s=s' \} \\ | ||
- | R_c(\mbox{assume}\ F}) &=& \{(s,s') \mid OK\ \rightarrow\ (F(s) \land s=s') \} \\ | ||
- | R_c(c_1 [] c_2) & = & R_c(c_1) \cup R_c(c_2) \\ | ||
- | R_c(c_1\ ;\ c_2) & = & R_c(c_1) \circ R_c(c_2) | ||
- | \end{eqnarray*} | ||
- | |||
- | ===== References ===== | ||
- | |||
- | * {{sav08:backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}} |