Re: SPARK

["Peter C. Chapin" <pcc482719@gmail.com>]

Yannick Duchêne (Hibou57) wrote:

> Is that this “cut point” which makes Simplifier to forget about previous  
> hypotheses when “assert” is used ? (if that's really similar to Prolog's  
> cut, then indeed, it likely to make the prover loose memory)
> 
> About one of the most worthy thing with proving : what's the better way to  
> give hints to the prover ? Is it “assert” or “check” ? This example  
> suggest the best way is “check”. Is this example representative of most  
> cases or a just a special case ?

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 which is clearly a problem
(since loops iterate a dynamic number of times). The assert "cuts" the loop
and reduces the problem to just

1. The path into the loop for the first time to the assert.
2. The path around the loop from assert to assert.
3. The path from the assert to whatever follows the loop.

It is necessary, I think, for SPARK to forget about previous "stuff" when
handling the assert since otherwise it would have to consider all the
previous loop iterations.

The check annotation asks SPARK to prove the check and then it can *add* that
information to the hypotheses of the following verification conditions rather
than start from scratch.

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.
I'm learning as well.

Peter