SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 16 May 2010 01:28 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 16 May 2010 14:13 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 16 May 2010 14:17 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 16 May 2010 20:59 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 16 May 2010 21:24
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.. |