Re: SPARK loop VCs that go "one beyond" the loop?

[mark.lorenzen@gmail.com]

Den søndag den 4. marts 2012 20.44.41 UTC+1 skrev Peter C. Chapin:
> 
> That worked! However, I'm still trying to understand the general 
> principle that can guide me in these situations. I feel like I have to 
> resort to semi-random attempts until I stumble into something that works.

Peter,

I strongly recommend Phil's proof tutorials that can be found here: http://www.sparksure.com/7.html

Try and have a look at chapters 7 and 8 in order to understand how the examiner transforms loop constructs into a standard form, from which it generates VCs. This should help you understand where invariants can be placed and what they should express.

Regards,

Mark L