SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 15 May 2010 14:00 > It was not able to prove it. Do I miss something or does it simply means > the simplifier does not know about a rule which seems basic to me, that > is (A <= B) -> ((A / C) <= (B / C)) ? ... which is still valid for > integer arithmetic. Sorry for a mistake, it should have been ((A <= B) and (A >= 0) and (C > 0)) -> ((A / C) <= (B / C)), to keep it simple and just to talk about what's relevant here. -- There is even better than a pragma Assert: an --# assert
From: Yannick Duchêne (Hibou57) on 15 May 2010 14:14 Another example, as much strange to me. 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); Part := Local_Data - Lowest; Whole := Highest - Lowest; --# assert Part >= 0; --# assert Local_Data <= Highest; -- .... The simplifier cannot prove âLocal_Data <= Highestâ, although the post condition of Limit states âX in Lower .. Upperâ so that it should know âLocal_Data in Lowest .. Highestâ and then âLocal_Data <= Highestâ. While perhaps I'm not using it the good way (as a beginner, this may be a possible case). -- There is even better than a pragma Assert: an --# assert
From: Phil Clayton on 15 May 2010 14:43 On May 15, 5:41 pm, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > > --# assert ((Part * 100) <= (Whole * 100)) -> > --# (((Part * 100) / Whole) <= ((Whole * 100) / Whole)); > > It was not able to prove it. Do I miss something or does it simply means > the simplifier does not know about a rule which seems basic to me, that is > (A <= B) -> ((A / C) <= (B / C)) ? ... which is still valid for integer > arithmetic. This isn't valid for all values of A, B and C: consider C = -1. It would be sufficient to know 0 < C, so perhaps sufficient information needs to be propagated to show 0 < Whole ? Phil C.
From: Yannick Duchêne (Hibou57) on 15 May 2010 15:08 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). When (2) is there, it seems to forget about the previously proved hypothesis (1) or about hypotheses which make (1) provable. Will have to better understand how this âthingâ thinks. -- There is even better than a pragma Assert: an --# assert
From: Yannick Duchêne (Hibou57) on 15 May 2010 15:12
> This isn't valid for all values of A, B and C: consider C = -1. It > would be sufficient to know 0 < C, so perhaps sufficient information > needs to be propagated to show 0 < Whole ? > > Phil C. Yes, you are right, that's why I had previously apologized for this error and corrected it in a reply to the erroneous message. Your exercises are interesting BTW. -- There is even better than a pragma Assert: an --# assert |