Differences
This shows you the differences between two versions of the page.
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); | ||