This is an old revision of the document!

Backward VCG with Loops

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.

Static single assignment form.