SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 14 May 2010 10:47 Le Thu, 13 May 2010 22:05:05 +0200, Rod Chapman <roderick.chapman(a)googlemail.com> a écrit: > We have now switched to use "-" on all platforms, so it's best > to use "-" on Windows now... > - Rod At least with the integration to GPS on Windows, the project properties tab for Examiner, does not work if "-" is used : option not recognized and no feed back in the sheet view. Only "/" works there (may be this is different now with SPARK 9, I don't know). An example to check : in the command line options input field (at the bottom), writing â-index_file=my_index.idxâ, makes the the corresponding input field to become empty (at the top of the property sheet), and it comes back if â-index_fileâ is replaced with â/index_fileâ. -- There is even better than a pragma Assert: an --# assert
From: Yannick Duchêne (Hibou57) on 14 May 2010 17:45 Anecdotal comment, surely not so much important :p In multiple places in various documentations (of any sources), a sentence similar to âProved by the Proof Checkerâ is used. Shouldn't this be âProved with the Proof Checkerâ instead ? ... as the Proof Checker requires human interventions and is not automated. -- There is even better than a pragma Assert: an --# assert
From: Yannick Duchêne (Hibou57) on 14 May 2010 18:55 Le Thu, 13 May 2010 05:06:23 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Block statements are not allowed in SPARK. Let say a procedure can do > the same. Was this only to have one-matter-one-feature (avoid to have > both block-statement and procedure, and keep only one) for the sake of > simplicity or was there some other reasons properly dealing with > verifiability ? Here is an answer: A document from SparkSure ( http://www.sparksure.com/7.html ), namely Part4_Multiple_Paths.pdf, warns about consecutive conditional statements, giving the example of ten simple chained If statement which turns into 1024 validation conditions. In this document, Phil logically advice to avoid such cases, using small procedures instead. Doing so, you end up with a single path instead of 1014. So far this is not about blocks, however here comes the matter: block statements does not break such a chain of If statements and cannot be given annotations. Lack of annotations with block statement makes these ineffective to reach the goal of simplifying the program provability. So why not annotations on block statements ? Well, simply because a block statement does not come with a signature and using a procedure instead of a block statement, requires you to better specify what was the role of that block. And adding extra-annotations to the language, to be used with blocks, would just load the language with unnecessary complications (not welcome in this area) Finally, block statements are disallowed to help avoid explosive complexity. -- There is even better than a pragma Assert: an --# assert
From: Peter C. Chapin on 15 May 2010 09:09 Yannick Duchêne (Hibou57) wrote: >> >> f(g(I) + f(f(g(I)))**2, >> >> or to >> >> f(f(g(I))) + f(g(I))**2. > A function optimized (which save computing of already computed inputs) > using memoisation, does not exposes this behavior. If it works properly, yes, but what if it doesn't? > How to make it formal : may be giving the proof the function is the only > one to access memoisation storage between function invokation, so, that > this data are mechanically private to the function. Then, demonstrate > there is two paths to the result : one which is the basic computation and > one which retrieve the result of a similar previous computation. This > latter step could rely on the computation of a key to access this data. > Then demonstrate that for a given input, the computed key is always the > same (input <-> key association). Now, the hard part may be to demonstrate > the key is used to access the result which was computed previously for the > same input that the one which was used to compute the key. > > Obviously, the function should be the only one to access this data. > > There is a concept in SPARK, the one of variable package and > state-machines. May be there could be some room for a concept which could > be something like function-package ? While this might be possible, it does sound rather complicated. I can see why SPARK doesn't currently go down this path. Peter
From: Yannick Duchêne (Hibou57) on 15 May 2010 12:41
Currently, I'm reading Phil's documents, the ones in the directory Proof_Annotations and especially looking at exercises (yes, he created some) in part 5 to 9 and 12. Part 5, exercise 4, turns to be something interesting to me, as it leads me to some questions about the way the simplifier is using hypothesis. I would like to be more explicit. Here is the relevant part (slightly modified) --------------------------------------------------------------------- -- Exercise 5.4 --------------------------------------------------------------------- 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 -- (1) --# ((Highest - Lowest) <= Integer'Last) and -- (2) --# (((Highest - Lowest) * 100) <= Integer'Last); -- (3) --# is Local_Data : Integer; Part : Integer; Whole : Integer; begin Local_Data := Data; -- (4) Limit (Local_Data, Lowest, Highest); -- (5) Part := Local_Data - Lowest; -- (6) Whole := Highest - Lowest; -- (7) return Percent_Type((Part * 100) / Whole); -- (8) end Percent_Of_Range; What's funny here, is about precondition line (2). If it is removed, the precondition become â(Lowest < Highest) and (((Highest - Lowest) * 100) <= Integer'Last)â and the simplifier fails to prove line (6) : it cannot prove the result will be lower than Integer'Last. I first though â(Highest - Lowest) * 100 <= Integer'Lastâ would be enough to also implies âHighest - Lowest < Integer'Lastâ ; it seems it is not. If you add precondition part (2), there is no more trouble with line (6). Is this because of the way it is using hypotheses or is this because it miss some built-in rules to get all benefits from precondition part (3) ? Now, there is still another unproved condition... at line (8), the simplifier cannot prove â((Local_Data - Lowest) * 100) / (Highest - Lowest) <= 100â. A first anecdote : funny to see it has expanded variables Part and Whole. I wanted to solve in three steps and added the following between (6) and (7) --# assert Part <= Whole; -- (6.1) --# assert (Part * 100) <= (Whole * 100); -- (6.2) --# assert ((Part * 100) / Whole) <= ((Whole * 100) / Whole); -- (6.3) But the simplifier was not able to prove (6.1) nor (6.3) and was still not able to prove (8). About (6.2), and wanted to have a test, and added the following between (6.2) and (6.3): --# 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. -- There is even better than a pragma Assert: an --# assert |