SPARK code samples
in [ADA]
|
Prev: Ada 2012: An Oops in the new Ada amendments ? (in 10.1.2 Context Clauses - With Clauses)
Next: Generic_Roots
From: Maciej Sobczak on 12 Aug 2010 03:29 On 12 Sie, 04:39, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > * I could have made a test to ensure inputs of A and B is in -1000..+1000, > while this would not avoid the need to check for the sum validity, as > formally speaking there is no way to assert anything on Integer range. > Second reason to dropped this assumption. OK ? No. AARM 3.5.4/21 defines the minimum range for Integer, it is -2**15+1..2**15-1. Since SPARK is supposed to be compilable as a valid Ada, then its implementation ranges cannot be smaller than those required for Ada and therefore you can safely assume that if A and B are within -1000..1000, then their sum will fit within Integer (their product might not). That will reduce the code significantly. I also think that if the program requirements say that the input will be in some range, you can assume this is true without asserting it. The point is that such requirements are verifiable outside of the program, for example by the design of subsystem (hardware data source, perhaps?) that feeds input to your component. Another argument might be the following: if you are not comfortable assuming that input is in the range defined externally, then why do you assume that the reaction of your program (printing English prose) will be valid in that same environment? The environment is not necessarily an English-speaking human sitting in front of the screen - especially in the case of SPARK programs. ;-) -- Maciej Sobczak * http://www.inspirel.com YAMI4 - Messaging Solution for Distributed Systems http://www.inspirel.com/yami4
From: Jacob Sparre Andersen on 12 Aug 2010 05:46 Yannick Duch�ne wrote: > Ok. I choose a first one, the one named A+B: > http://rosettacode.org/wiki/A%2BB#Ada [...] I think you have made the problem much too complicated. Isn't this sufficient? (I haven't got a SPARK Examiner right here.) ------------------------------------------------------------ with SPARK_IO; --# inherit SPARK_IO; --# main_program; procedure A_Plus_B --# global in out SPARK_IO.Inputs, SPARK_IO.Outputs; --# derives SPARK_IO.Inputs from SPARK_IO.Inputs & --# SPARK_IO.Outputs from SPARK_IO.Inputs, SPARK_IO.Outputs; is subtype Small_Integers is Integer range -1_000 .. +1_000; A, B : Integer; A_OK, B_OK : Boolean; begin SPARK_IO.Get_Integer (File => SPARK_IO.Standard_Input, Item => A, Width => 0, Read => A_OK); A_OK := A_OK and A in Small_Integers; SPARK_IO.Get_Integer (File => SPARK_IO.Standard_Input, Item => B, Width => 0, Read => B_OK); B_OK := B_OK and B in Small_Integers; if A_OK and B_OK then SPARK_IO.Put_Integer (File => SPARK_IO.Standard_Output, Item => A + B, Width => 4, Base => 10); else SPARK_IO.Put_Line (File => SPARK_IO.Standard_Output, Item => "Input data does not match specification.", Stop => 0); end if; end A_Plus_B; ------------------------------------------------------------ Kind regards, Jacob Sparre Andersen -- Jacob Sparre Andersen Research & Innovation Vesterbrogade 148K, 1. th. 1620 K�benhavn V Danmark Phone: +45 21 49 08 04 E-mail: jacob(a)jacob-sparre.dk Web-site: http://www.jacob-sparre.dk/
From: Ada novice on 12 Aug 2010 08:08 On Aug 11, 8:21 pm, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Le Wed, 11 Aug 2010 19:10:22 +0200, Ada novice <ycalleecha...(a)gmx.com> a > écrit:>http://www.stsc.hill.af.mil/crosstalk/2006/09/0609swardgerkencasey.html > > Thanks for this one YC. I will enjoy reading it. > You're welcome. And thanks for the link to the tutorials by Phil Thornley (http://www.sparksure.com/) that you provided some time back at fr.comp.lang.ada YC
From: Yannick Duchêne (Hibou57) on 12 Aug 2010 09:31 Le Thu, 12 Aug 2010 07:02:22 +0200, Jeffrey Carter <spam.jrcarter.not(a)spam.not.acm.org> a écrit: > A .. B is the null range. I think you meant B .. A. Yes. Erroneous copy/paste of a similar comment above or below. This kind of error cannot be checked by SPARK :p Apologize. -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Yannick Duchêne (Hibou57) on 12 Aug 2010 09:41
Le Thu, 12 Aug 2010 09:29:22 +0200, Maciej Sobczak <see.my.homepage(a)gmail.com> a écrit: > No. AARM 3.5.4/21 defines the minimum range for Integer, it is > -2**15+1..2**15-1. I was aware of that for Ada, while not sure for SPARK, as this depends on a machine description file. Will suppose it in the future. > I also think that if the program requirements say that the input will > be in some range, you can assume this is true without asserting it. > The point is that such requirements are verifiable outside of the > program, for example by the design of subsystem (hardware data source, > perhaps?) that feeds input to your component. OK, I see. That is a clever point (I had never operate in a staff, so I could not know that). > The environment is not > necessarily an English-speaking human sitting in front of the screen - > especially in the case of SPARK programs. ;-) Assumed that if there is a SPARK_IO, this ends into something which is not dropped (either screen, file, single line text display, any) Good point anyway. -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. |