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 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)
wp(assert(false); assume(false),Q) = false wp(assume(false); assert(false),Q) = true
so cannot have any more, otherwise both
assert(false); assume(false) assume(false); assert(false)
would denote empty relations.
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 satisfy
Desired Rules for Weakest Preconditions
For all such that , we would like the following to hold:
We assume above that is not the error variable.
Note: we wrote in the weakest precondition of assume, but usually is implicit and we do not write it. We do not need it in other cases because it follows that right hand side implies .
Relational Semantics that Fulfills These Rules
Let OK denote s(error)=0 and OK' denote s'(error)=0. We define: