SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 15 May 2010 16:23 Le Sat, 15 May 2010 21:08:05 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Oh, something interesting: > > > procedure Limit > (X : in out Integer; > Lower : in Integer; > Upper : in Integer) > --# pre Lower < Upper; > --# post ((X~ < Lower) -> (X = Lower)) and > --# ((X~ > Upper) -> (X = Upper)) and > --# (X in Lower .. Upper); > > -- ..... > > > Limit (Local_Data, Lowest, Highest); > --# assert Local_Data <= Highest; -- (1) > Part := Local_Data - Lowest; > Whole := Highest - Lowest; > --# assert Part >= 0; -- (2) > --# assert Local_Data <= Highest; -- (3) > > -- ..... > > > If (2) is removed, it can prove (1) and (3). If (2) is there, it fails > to prove (3), while nothing changes Local_Data in the path from (1) to > (3), and so (3) should be as much provable as (1). If âassertâ is replaced by âcheckâ then it can prove (3) even if (2) is there. So that procedure Limit (X : in out Integer; Lower : in Integer; Upper : in Integer) --# pre Lower < Upper; --# post ((X~ < Lower) -> (X = Lower)) and --# ((X~ > Upper) -> (X = Upper)) and --# (X in Lower .. Upper); -- ..... Limit (Local_Data, Lowest, Highest); --# check Local_Data <= Highest; -- (1) Part := Local_Data - Lowest; Whole := Highest - Lowest; --# check Part >= 0; -- (2) --# check Local_Data <= Highest; -- (3) -- ..... is OK. So let's talk about âassertâ vs âcheckâ. [Generation of VCs for SPARK Programs (2.2)] says: > each assert or check statement in the code is located at a point in > between two executable statements, in general, ie it is associated > with a point on the arc of the flowchart of the subprogram which > passes between the two statements it appears between. Each such > assertion specifies a relation between program variables which must > hold at that precise point, whenever execution reaches it. Assert > statements generate a cut point on the flowchart of the subprogram, > check statements do not. 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. 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 ? -- There is even better than a pragma Assert: an --# assert (or a --# check.... question pending)
From: Phil Clayton on 15 May 2010 17:02 On May 15, 8:12 pm, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Yes, you are right, that's why I had previously apologized for this error > and corrected it in a reply to the erroneous message. Yes, I hadn't updated the web page to see your latest message. > Your exercises are interesting BTW. They're not mine - I'm a different Phil! An unfortunate overloading issue here... Phil C.
From: Yannick Duchêne (Hibou57) on 15 May 2010 18:48 Ok, from some branch of this thread, you may have learned a question have raised about which one of âassertâ or âcheckâ should be used to write in-text proofs where the Simplifier could not prove it it/his/her self. The answer to this is so much important that I give the answer to it from the root of this thread, instead of from the latter leaf. So it is : Use Check, not Assert. Here is a concrete example of what you can do with Check and which does not work with Assert. The example is detailed, I mean, exposes detailed proofs, over what may have been sufficient. This is because I like explicit and expressive things, and this was also to be sure nobody could miss a single step of the proof and nobody could have any doubt about the usefulness of such a approach in software conception. That's also the reason why the exercise upon which this is based, was a bit modified (like using two intermediate variables instead of subexpressions.. I do that oftenly on my side). Here is : procedure Limit (X : in out Integer; Lower : in Integer; Upper : in Integer) --# pre Lower < Upper; --# post ((X~ < Lower) -> (X = Lower)) and --# ((X~ > Upper) -> (X = Upper)) and --# (X in Lower .. Upper); is begin if X < Lower then X := Lower; elsif X > Upper then X := Upper; end if; end Limit; function Percent_Of_Range (Data : Integer; Lowest : Integer; Highest : Integer) return Percent_Type --# pre (Lowest < Highest) and --# ((Highest - Lowest) <= Integer'Last) and --# (((Highest - Lowest) * 100) <= Integer'Last); is Local_Data : Integer; Part : Integer; Whole : Integer; begin Local_Data := Data; -- Local copy of Data to be allowed to modify it. We only need -- a modified version locally, the caller does not need this. Limit (X => Local_Data, -- in out. Lower => Lowest, -- in Upper => Highest); -- in. Part := Local_Data - Lowest; Whole := Highest - Lowest; -- We are to prove that ((Part * 100) / Whole) is in 0 .. 100. -- (1) Prove that Part >= 0. --# check Local_Data in Lowest .. Highest; --# check Local_Data >= Lowest; --# check (Local_Data - Lowest) >= 0; --# check Part >= 0; -- Given (1), it's obvious that (Part * 100) >= 0. -- (2) Prove that Whole is > 0. --# check Lowest < Highest; --# check Highest > Lowest; --# check (Highest - Lowest) > 0; --# check Whole > 0; -- Given (2), it's obvious that ((Part * 100) / Whole) is valid. -- Given (1) and (2), it's obvious that ((Part * 100) / Whole) >= 0. -- (3) Prove that (Whole >= Part). This is required for (4) which is -- to come. --# check Local_Data in Lowest .. Highest; --# check Highest >= Local_Data; --# check (Highest - Lowest) >= (Local_Data - Lowest); --# check Whole >= Part; -- (4) Prove that ((Part * 100) / Whole) is less or equal to 100. --# check Part <= Whole; --# check (Part * 100) <= (Whole * 100); --# check ((Part * 100) / Whole) <= ((Whole * 100) / Whole); --# check ((Part * 100) / Whole) <= 100; -- (5) Prove that the subexpression (Part * 100) will not -- commit an overflow. --# check (((Highest - Lowest) * 100) <= Integer'Last); --# check (Whole * 100) <= Integer'Last; --# check Part <= Whole; --# check (Part * 100) <= Integer'Last; -- Given (1), we know ((Part * 100) / Whole) >= 0. -- Given (4), we know ((Part * 100) / Whole) <= 100. -- Given (5), we we know (Part * 100) will not commit an overflow.. -- Given (1) and (2) and(5), the following statement is then proved to -- be valid and meaningful. return Percent_Type ((Part * 100) / Whole); end Percent_Of_Range; A working example of a step by step proof of every things required to be proven. Waaw... I like it so much, I love it. This is the way I was thinking software should be built for so long ! I was waiting for such a thing for about 14 years you know ! I use to learn about VDM when I was younger, hire books about it in libraries, use to think about creating my own implementation of VDM, but failed to find the language specification (and was frightened about the idea to setup my own language in this area). And now, I see SPARK can do nearly the same. Well, although wonderful, that's still not perfect : why is there a Checker (which I didn't used here) and why no provision to write in-text what is done with the Checker ? That's what I was attempting to do here. It works, but I miss something like explicit âfrom (1) and (2) infer .... â etc. I cannot give names or numbers to Check clauses and cannot explicitly refer to these. I cannot nor explicitly refer to precondition in inferences (like in (5), where the reference to a precondition is implicit, not explicit). Is there some provision for such a thing ? Yes, I may wish too much... that's not perfect, while still wonderful. Do you feel too ? :) -- There is even better than a pragma Assert: an --# assert (or a --# check... question pending)
From: Yannick Duchêne (Hibou57) on 15 May 2010 21:48 Le Sun, 16 May 2010 00:48:33 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Ok, from some branch of this thread, you may have learned a question > have raised about which one of âassertâ or âcheckâ should be used to > write in-text proofs where the Simplifier could not prove it it/his/her > self. > > The answer to this is so much important that I give the answer to it > from the root of this thread, instead of from the latter leaf. > > So it is : Use Check, not Assert. > [...] Part 6 of Phil's document says: > For both check and assert, there is a VC generated that has > the current program state as hypotheses and the <Boolean > expression> as the conclusion. I've meet something different (see previous messages in this thread), or at least, the current state is not represented with the same set of hypotheses. > For code that does not contain any loops, there is > (in principle) never any need for either of these > annotations since they cannot make unprovable VCs > into provable VCs. Sorry, I can't buy that at all. I could make VCs provable, and this was otherwise not provable by the simplifier, using Check clauses. Sorry friend, I'm not dreaming : this really happened. -- 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 15 May 2010 21:53
> Sorry, I can't buy that at all. I could make VCs provable, and this was > otherwise not provable by the simplifier, using Check clauses. > > Sorry friend, I'm not dreaming : this really happened. No, OK, I'm wrong : miss-understood the meaning of unprovable in this context. You're OK. -- 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. |