LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:verifying_programs_with_global_containers [2008/04/03 13:51]
vkuncak created 		sav08:verifying_programs_with_global_containers [2008/04/03 16:16] (current)
vkuncak
Line 2: Line 2:
  
 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. 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);