From: Yannick Duchêne (Hibou57) on
Request for confirmation.

In Praxis's documentations, there is a file named Checker_Rules.pdf, title
is “SPADE Proof Checker Rules Manual”, which list Checker's built-in
rules. I do not see any reason why the Examiner/Simplifier would have a
different rules set than the Checker, so I suppose this rules set is also
the one used by the Examiner/Simplifier. I would just want to be sure :
someone can confirm ?

If it is, this may explain why I meet some troubles proving one thing with
real arithmetic (yes, I know real arithmetic is not safe and I must care,
but this is just an exercise...)

--
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..
From: Peter C. Chapin on
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

From: Phil Thornley on
On 15 May, 21:23, Yannick Duchêne (Hibou57) <yannick_duch...(a)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
From: Yannick Duchêne (Hibou57) on
Le Sun, 16 May 2010 20:13:27 +0200, Peter C. Chapin <pcc482719(a)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..
From: Yannick Duchêne (Hibou57) on
Le Sun, 16 May 2010 20:17:49 +0200, Phil Thornley
<phil.jpthornley(a)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..