This is an old revision of the document!
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.