LARA

Verifying Programs with Global Containers

If instead of integers, our programs manipulate sets, the verification conditions will be in the set language and we can decide them by translation into exists-forall class.

Example: showing that a program that takes elements from set A and sorts into sets B and C, never loses any elements.

 A = A0;
 B = {};
 C = {};
 while //: inv "..."
   (A != {}) {
   pick x in A;
   if (condition(x)) {
     B = B union {x};
   } else {
     C = C union {x};
   }
 }
 assert(B union C = A0);