LARA

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.

Encoding Interactive Proof Commands into Programs