SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 13 May 2010 12:48 Le Thu, 13 May 2010 11:28:03 +0200, <stefan-lucks(a)see-the.signature> a écrit: > When working with SPARK, it is difficult *not* to face that. E.g., > usually, you would write a pseudorandom number generator as > > function Rnd return T is > begin > Global_State := f(Global_State); > return g(Global_State); > end; > > In SPARK, you have to replace the function RND by a procedure, which > delivers the result as an out parameter. Yes, an example from Barnes gives the same: Quote from http://people.cis.ksu.edu/~hatcliff/890-High-Assurance/Slides/Barnes-Ch-02-Language-Principles.pdf package Random_Numbers --# own Seed; --# initializes Seed; is procedure Random(X: out Float); --# global in out Seed; --# derives X, Seed from Seed; end Random_Numbers; package body Random_Numbers is Seed: Integer; Seed_Max: constant Integer := ⦠; procedure Random(X: out Float) is begin Seed := ⦠; X := Float(Seed) / Float(Seed_Max); end Random; begin -- initialization part Seed := 12345; end Random_Numbers > Very inconvenient! But reasonable: For that purpose, yes, as a radom generator is not a pure function. > Note that the result from evaluating an expression such as "Rnd + Rnd**2" > depends on the order of evaluation, which isn't specified in the Ada > standard. If we write I for the initial global state, then "Rnd + Rnd**2" > can either evaluate to > > 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. > Such an unspecified behaviour makes static analysis very difficult. In > principle, you would have to consider all possible orders of evaluation > and check if something is going wrong. That would be very hard for SPARK, > and, with a few legitimate exceptions, such that pseodorandom numbers, > this is bad programming style anyway. Thus, SPARK prohibits this. Indeed, there should not be any attempt to make proof on a language which would allow function whose result depends on the invokation time-stamp, and so whose result may depend on evaluation order. Functions using memoisation are different case and are still pure function. What change between each invokation, is not the result, just the time to compute it (which may be shorter for some next invokation). 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 ? Just some seed of an idea... will think about it some later day -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 13 May 2010 12:54 An AdaCore/Praxis webinar, talks about a tool which make VCG files more readable, producing a graph representation of these, using GraphViz. This looks useful. Go there to read or hear about it : http://www.adacore.com/home/products/gnatpro/webinars/ and choose âGetting started with SPARK (October 13, 2009)â, that's about in the last third part. However, I was not able to find this in the SPARK installation directory and did not find more on the web. Do someone know any points, docs or links ? That's not required to run the Examiner nor the Simplifier, I know, however this really seems to make things more readable. -- pragma Asset ? Is that true ? Waaww... great
From: Rod Chapman on 13 May 2010 13:15 On May 13, 5:54 pm, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > An AdaCore/Praxis webinar, talks about a tool which make VCG files more > readable, producing a graph representation of these, using GraphViz. This > looks useful. Run the Examiner with -vcg -debug=V (see section 3.1.4 of the Examiner User Manual)... Then go grab GraphViz from www.graphviz.org Have fun... - Rod Chapman, SPARK Team, Praxis
From: Yannick Duchêne (Hibou57) on 13 May 2010 15:43 > Run the Examiner with -vcg -debug=V > (see section 3.1.4 of the Examiner User Manual)... OK. I had seen the debug option from the help command and though this was not the good one. Finally, this is the âdebug=dâ which produce dot files for GraphViz. However, the v and V values also gives readable output in the form of a list (raw text). Note for the Windows platform : the prefix for SPARK's command line switches is "/" instead of "-" ("/" is indeed the native Windows style for command line options). > Have fun... For sure I will :) -- pragma Asset ? Is that true ? Waaww... great
From: Rod Chapman on 13 May 2010 16:05
On May 13, 8:43 pm, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > > Run the Examiner with -vcg -debug=V > > (see section 3.1.4 of the Examiner User Manual)... > > OK. I had seen the debug option from the help command and though this was > not the good one. > Finally, this is the debug=d which produce dot files for GraphViz.. > However, the v and V values also gives readable output in the form of a > list (raw text). -debug=d dumps expression DAGS in DOT format. -debug=v or V produces output on the screen AND also produces DOT format for the VCG graph(s) alongside the generated .vcg files. if you use -debug=V and then look at the sequence of generated graphs in numerical order, you'll see how the VC-generator works! > Note for the Windows platform : the prefix for SPARK's command line > switches is "/" instead of "-" ("/" is indeed the native Windows style for > command line options). We have now switched to use "-" on all platforms, so it's best to use "-" on Windows now... - Rod |