Re: SPARK

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

Le Sun, 16 May 2010 20:17:49 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> [...]
> 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 - [...]
Otherwise this would not be a cut-point any more, indeed, and starting  
with a new state, is not a side effect, it's the purpose.

> 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.)
Unfortunately, I wanted to prove every things (cheese)

TBH, I did not work on all, just some and just had a quick overview on  
others.

> There are (at least) three ways to deal with these (other than
> changing the code itself).
Sorry for that Er Professor, I've modified it a bit (re-cheese).

> 1) Give the Simplifier 'hints' by adding check annotations.
> 2) Use the Proof Checker to prove the VCs left after simplfication.
As said in another message, this was exactly the purpose : I wanted to  
prove without relying on the Checker, in order to have all proofs in the  
text. It seems to be possible, as long as one is explicit enough.

> 3) Give the Simplifier more rules to use ('user rules').
I would better like add a very few rule in the whole system, better than  
adding some rules here and there, all being package specific.

> My experience is that trying 1) can get very frustrating as the
> Simplifier sometimes seems to be extremely stupid.
That's an important matter. On an other thread, on the french c.l.a (where  
I’ve talked about the same), I was afraid some people may think SPARK is  
not working properly and is unusable for that reason. That's why I  
insisted a lot on the Check clause and to not be afraid to detail proofs  
as much as needed.

> 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.)
I would prefer the choice #3, which seems more logical to me. Just that  
this may be better to add these rules system wide better than on a package  
basis. If I'm not wrong, there is provision for that also.

The requirement for a rule to be sound, is indeed important. There may be  
some rule of thumb in that area, like check all special cases, all special  
ranges. As an example, before adding a rule on real, one may carefully  
check the rule is valid for multiple combinations of special values and  
bounds and range on each items appearing in the rule, like 0, 1, -1, 0 ..  
1, 0 .. -1, > 1, < -1, and so on. The same with set, there are special  
values as well : empty set/sequence, one element set/sequence, more than  
one, a set included in an other, etc.

In that area, I was wondering how built-in rules were  choose : from a  
well know set of scientist ? Empirically ? By expansion during SPARK's  
life ? Others ?

I was wondering about it, because I could not find one rule which seems  
important to me, and which does not seems to be part of the predefined set  
(well, there are actually +500 rules, however, may be some useful rules  
are still missing).

> (If you are working through the tutorials in sequence then user rules
> are in section 11 - the next to the last).
Yes, I've seen it, and I've also read Part 6, which is about the  
difference between Check and Assert (I've it later after the question you  
were answering).

Have a nice day (Peter as well, obviously)

Yannick D.

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