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: Yannick Duchêne (Hibou57) on 11 Aug 2010 14:21 Le Wed, 11 Aug 2010 19:10:22 +0200, Ada novice <ycalleecharan(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. -- 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 11 Aug 2010 22:39 Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov <mailbox(a)dmitry-kazakov.de> a écrit: > http://rosettacode.org/wiki/Category:Programming_Tasks > > (the first 200 (:-)) > > Pick any you wish. Ok. I choose a first one, the one named A+B: http://rosettacode.org/wiki/A%2BB#Ada I felt it was interesting because it deals with a case of simple I/O, which is a first-time issue with SPARK, and because there was the opportunity to expose a simple case of validity check. However, I don't want to post it there straight away, as I came to two dirty questions. First the implementation I end up with, then the two questions. -------------------------------------------------------------------- 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 A : Integer; B : Integer; Sum : Integer; Process_Is_Valid : Boolean; Input_Is_OK : Boolean; A_And_B_Sumable : Boolean; begin Process_Is_Valid := True; -- Attempt to Read A from Standard Input. SPARK_IO.Get_Integer (File => SPARK_IO.Standard_Input, Item => A, Width => 0, Read => Input_Is_OK); if not Input_Is_Ok then Process_Is_Valid := False; end if; -- Attempt to Read B from Standard Input. B := 0; if Process_Is_Valid then SPARK_IO.Get_Integer (File => SPARK_IO.Standard_Input, Item => B, Width => 0, Read => Input_Is_OK); if not Input_Is_Ok then Process_Is_Valid := False; end if; end if; -- Get A + B checking the sum is valid in the while. Sum := 0; if Process_Is_Valid then A_And_B_Sumable := False; if A >= 0 and B >= 0 then if (Integer'Last - A) >= B then Sum := A + B; A_And_B_Sumable := True; end if; elsif A >= 0 and B < 0 then -- Always valid as the sum is -- in range A..B Sum := A + B; A_And_B_Sumable := True; elsif A < 0 and B >= 0 then -- Always valid as the sum is -- in range A..B Sum := A + B; A_And_B_Sumable := True; elsif A < 0 and B < 0 then if (Integer'First - A) <= B then Sum := A + B; A_And_B_Sumable := True; end if; end if; if not A_And_B_Sumable then Process_Is_Valid := False; end if; end if; -- Write A + B. if Process_Is_Valid then SPARK_IO.Put_Integer (File => SPARK_IO.Standard_Output, Item => Sum, Width => 0, Base => 10); else SPARK_IO.Put_Line (File => SPARK_IO.Standard_Output, Item => "Either the input or the sum was invalid.", Stop => 0); -- 0 means no extra spaces will be written. end if; end A_Plus_B; -------------------------------------------------------------------- Questions: * The page says the input of both A and B is supposed to be in range -1000..+1000. Obviously there is no way to assert this, so I simply dropped the assumption. Are you OK ? * 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 ? This case apart, I was thinking giving SPARK examples there, we may not rely on user defined rules nor on the checker. Things should be provable as-is. -- 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 11 Aug 2010 23:03 Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov <mailbox(a)dmitry-kazakov.de> a écrit: Look at that : http://rosettacode.org/wiki/Comments#Ada For Algol60, it says: ⢠The original way of adding your 2 cents worth to a program with the "cent" character ¢â Now every one can understand the meaning of âmy 2 centsâ :D Funny -- 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: Jeffrey Carter on 12 Aug 2010 01:02 > elsif A >= 0 and B < 0 then > -- Always valid as the sum is > -- in range A..B A .. B is the null range. I think you meant B .. A. -- Jeff Carter "Hello! Smelly English K...niggets." Monty Python & the Holy Grail 08 --- news://freenews.netfront.net/ - complaints: news(a)netfront.net ---
From: cjpsimon on 12 Aug 2010 03:16
On 12 août, 04:39, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov > <mail...(a)dmitry-kazakov.de> a écrit:>http://rosettacode.org/wiki/Category:Programming_Tasks > > > (the first 200 (:-)) > > > Pick any you wish. > > Ok. I choose a first one, the one named A+B:http://rosettacode.org/wiki/A%2BB#Ada > > I felt it was interesting because it deals with a case of simple I/O, > which is a first-time issue with SPARK, and because there was the > opportunity to expose a simple case of validity check. > > However, I don't want to post it there straight away, as I came to two > dirty questions. First the implementation I end up with, then the two > questions. > > -------------------------------------------------------------------- > > 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 > A : Integer; > B : Integer; > Sum : Integer; > > Process_Is_Valid : Boolean; > Input_Is_OK : Boolean; > A_And_B_Sumable : Boolean; > > begin > Process_Is_Valid := True; > > -- Attempt to Read A from Standard Input. > > SPARK_IO.Get_Integer > (File => SPARK_IO.Standard_Input, > Item => A, > Width => 0, > Read => Input_Is_OK); > > if not Input_Is_Ok then > Process_Is_Valid := False; > end if; > > -- Attempt to Read B from Standard Input. > > B := 0; > > if Process_Is_Valid then > SPARK_IO.Get_Integer > (File => SPARK_IO.Standard_Input, > Item => B, > Width => 0, > Read => Input_Is_OK); > > if not Input_Is_Ok then > Process_Is_Valid := False; > end if; > end if; > > -- Get A + B checking the sum is valid in the while. > > Sum := 0; > > if Process_Is_Valid then > A_And_B_Sumable := False; > > if A >= 0 and B >= 0 then > if (Integer'Last - A) >= B then > Sum := A + B; > A_And_B_Sumable := True; > end if; > elsif A >= 0 and B < 0 then > -- Always valid as the sum is > -- in range A..B > Sum := A + B; > A_And_B_Sumable := True; > elsif A < 0 and B >= 0 then > -- Always valid as the sum is > -- in range A..B > Sum := A + B; > A_And_B_Sumable := True; > elsif A < 0 and B < 0 then > if (Integer'First - A) <= B then > Sum := A + B; > A_And_B_Sumable := True; > end if; > end if; > > if not A_And_B_Sumable then > Process_Is_Valid := False; > end if; > end if; > > -- Write A + B. > > if Process_Is_Valid then > SPARK_IO.Put_Integer > (File => SPARK_IO.Standard_Output, > Item => Sum, > Width => 0, > Base => 10); > else > SPARK_IO.Put_Line > (File => SPARK_IO.Standard_Output, > Item => "Either the input or the sum was invalid.", > Stop => 0); -- 0 means no extra spaces will be written. > end if; > > end A_Plus_B; > > -------------------------------------------------------------------- > > Questions: > > * The page says the input of both A and B is supposed to be in range > -1000..+1000. Obviously there is no way to assert this, so I simply > dropped the assumption. Are you OK ? > > * 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 ? > The RM : In an implementation, the range of Integer shall include the range 2**15+1 .. +2**151. > This case apart, I was thinking giving SPARK examples there, we may not > rely on user defined rules nor on the checker. Things should be provable > as-is. > > -- > 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. |