Backward VCG: Symbolic Execution using Weakest Preconditions
We again assume for simplicity to have two variables, .
Rules for Computing Weakest Preconditions
We derive the rules below from the definition of weakest precondition on sets and relations
Suppose we have one variable x, and identify state with that variable. By definition
Changing from sets to formulas (and keeping the same name), we obtain the rule for wp on formulas:
Consider the case of two variables. Recall that the relation associated with the assignment x=e is
Then we have, for formula containing and :
From here we obtain:
Same for formulas:
Nondeterministic Choice (Branches)
In terms of sets and relations
In terms of formulas
Size of Generated Verification Conditions
Because of the rule which duplicates , the size can be exponential.
- Calculus of Computation Textbook, Chapter 5 (Program Correctness: Mechanics)