Re: SPARK

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sun, 16 May 2010 20:13:27 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> My understanding is that assert prevents the simplifier from using  
> previous
> material as hypotheses in following verification conditions---as you  
> noticed
> in your experiments. John Barnes talks about this in his book a little.
> Mostly I think assert is intended for use in loops. Without it, SPARK  
> needs
> to consider each loop iteration as a spearate path
Here is the word, as you said, this cut the path. That's what I've learned  
later too. This starts a new path, with a new hypotheses set, and indeed,  
forget about all previous.

Now we know why it is so.

> [...]
> So to summarize perhaps a good rule might be to use assert to express  
> loop
> invariants and check for everything else. I welcome other comments on  
> this.
It seems all is there.

> I'm learning as well.
Great! Cheers


-- 
There is even better than a pragma Assert: a SPARK --# check.

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.