# 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

#### Assume Statement

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:

#### Assignment Statement

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:

#### Havoc Statement

#### Sequential Composition

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.

#### More information

- Calculus of Computation Textbook, Chapter 5 (Program Correctness: Mechanics)