Re: SPARK

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 15 May, 21:23, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[big snip :-]

> What does “cut point” means precisely ? Is it related or similar to the  
> unfortunately too much famous Prolog's cut ? This seems to be the next  
> question to be answered, and a focus to care about for peoples learning  
> SPARK.

There may be multiple paths to any point (before/after/between
executeable statements).  For the purposes of VC generation, a "cut
point" is a point in the code that terminates all the paths that reach
it and there is a single path starting at that point.

The hypotheses of VCs include the local state that has been defined
along a path, and each path to a point will have different versions of
these hypotheses.

Therefore the hypotheses that are generated in VCs that follow a cut
point cannot include any of the hypotheses that have been included in
the VCs before the cut point - unless they are included in the
assertion at the cut point and therefore proved to be true for every
path that reaches that cut point.


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

You should always use 'check' when giving the Simplifier a hint - then
you don't lose any of the local state information.

Another key point to understand is that the Simplifier does not prove
all provable VCs (so when the tutorials ask you to "make all VCs
provable" don't expect to get all the VCs proved by the Simplifier.)

There are (at least) three ways to deal with these (other than
changing the code itself).
1) Give the Simplifier 'hints' by adding check annotations.
2) Use the Proof Checker to prove the VCs left after simplfication.
3) Give the Simplifier more rules to use ('user rules').

My experience is that trying 1) can get very frustrating as the
Simplifier sometimes seems to be extremely stupid.
2) works OK but isn't practical for any software under development as
the proof scripts that are created (and are needed each time the VCs
are generated) are extremely fragile to minor changes in the software.
The current recommendation is to use 3) - create user rules as
appropriate.  These are easy to write and usually work as expected.
(But they are a very powerful mechanism, so are correspondingly
dangerous - it is quite easy to create unsound user rules.)

(If you are working through the tutorials in sequence then user rules
are in section 11 - the next to the last).

Cheers,

Phil