Re: SPARK

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

Le Sun, 16 May 2010 00:48:33 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Ok, from some branch of this thread, you may have learned a question  
> have raised about which one of “assert” or “check” should be used to  
> write in-text proofs where the Simplifier could not prove it it/his/her  
> self.
>
> The answer to this is so much important that I give the answer to it  
> from the root of this thread, instead of from the latter leaf.
>
> So it is : Use Check, not Assert.
> [...]

Part 6 of Phil's document says:

> For both check and assert, there is a VC generated that has
> the current program state as hypotheses and the <Boolean
> expression> as the conclusion.
I've meet something different (see previous messages in this thread), or  
at least, the current state is not represented with the same set of  
hypotheses.


> For code that does not contain any loops, there is
> (in principle) never any need for either of these
> annotations since they cannot make unprovable VCs
> into provable VCs.
Sorry, I can't buy that at all. I could make VCs provable, and this was  
otherwise not provable by the simplifier, using Check clauses.

Sorry friend, I'm not dreaming : this really happened.

-- 
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.