# Backward VCG with Loops

When using wp, we do not need to separately accumulate verification conditions, because we accumulate them all in the precondition formula.

## Desugaring loops with loop invariants

The following transformation is used in ESC/Java and Spec# to check loops with supplied loop invariants.

while [inv I] (F) c1

⇒

assert(I); havoc(x1,...,xn); (those that can be modified in the loop) assume(I); assume(~F);

Provided that I is inductive. We can check that I is inductive by proving:

assume(I); assume(F); c1; assert(I);

in isolation. Or proving

havoc(x1,...,xn) assume(I); assume(F); c1; assert(I);

at any point. If we combine these two, we get:

⇒

assert(I); havoc(x1,...,xn); assume(I); (assume(~F) [] assume(F); c1; assert I; assume(false));

Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. This can make loop invariant shorter.

## Avoiding Exponential Explosion

The tricks to avoid exponential explosion can also be implemented in backwards verification-condition generation, using a variant of static single assignment form.