SPARK code samples

SPARK code samples

[Dmitry A. Kazakov]

Since evidently growing interest in SPARK Ada and availability of public
SPARK compiler, I welcome those who are interested in learning and testing
SPARK to contribute their solutions to the Rosetta Code:

   http://rosettacode.org/wiki/Main_Page

The Rosetta Code has a half of thousand programming tasks defined. The
tasks are solved almost any programming language ever existed. Ada is well
represented in Rosetta, but SPARK is not. (Clearly, not all tasks could be
implemented in SPARK)

Rosetta is pretty liberal, everyone can register and contribute. The
SPARK's page is:

   http://rosettacode.org/wiki/SPARK

Thanks.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: SPARK code samples

[Ada novice]

On Aug 11, 10:44 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
>
> Rosetta is pretty liberal, everyone can register and contribute. The
> SPARK's page is:
>
>    http://rosettacode.org/wiki/SPARK

Thanks for this information. I'm interested to learn SPARK. If I
understand correctly, SPARK aligns itself well with Ada 95 and not yet
with Ada 05. Is this because of the strictness of SPARK to provide
highly reliable codes and hence it contains only well-tested features
(subset of Ada features)? It would be interesting to see some SPARK
codes on the wiki page building over time.

YC

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 13:38:36 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:
> Is this because of the strictness of SPARK to provide
> highly reliable codes and hence it contains only well-tested features
> (subset of Ada features)?

Yes, this is the main reason, while this is not a barrier. It also have to  
wait to be able to integrate Ada 2005, which cannot be done before the  
required art and technique is there.

That said, SPARK slowly evolves toward the last Ada revision. Have a look  
at this (just an example among others):
http://libre.adacore.com/libre/tools/spark-gpl-edition/

Which says
> A new SPARK 2005 language switch, enabling an initial set of
> new features for SPARK 2005. More features from Ada 2005 will
> be added to SPARK in future releases.

This cannot be done before proper formalization.... means this need time.

-- 
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.

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 10:44:58 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>    http://rosettacode.org/wiki/Main_Page
I use to see reference to it from place to place. Just have a quick look a  
few seconds ago. Is it on purpose if all examples seems to lack comments ?  
I do not see any unsolved task for SPARK. Will have to first look at how  
this site works prior anything.


-- 
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.

Re: SPARK code samples

[Mark Lorenzen]

On 11 Aug., 13:38, Ada novice <ycalleecha...@gmx.com> wrote:
>
> Thanks for this information. I'm interested to learn SPARK. If I
> understand correctly, SPARK aligns itself well with Ada 95 and not yet
> with Ada 05. Is this because of the strictness of SPARK to provide
> highly reliable codes and hence it contains only well-tested features
> (subset of Ada features)? It would be interesting to see some SPARK
> codes on the wiki page building over time.

Not quite. SPARK is a proper subset of Ada and is amenable to static
analysis. This has (in principle) nothing to do with if an Ada feature
is well-tested or not. You should think of SPARK as a language in its
own right and not as a subset of some other language. Although SPARK
constantly evolves it will never evolve into a language with the same
feature-set as Ada - no matter how well tested all Ada festures one
day will be.

Re: SPARK code samples

[(see below)]

On 11/08/2010 17:07, in article
fa1507ef-77a8-4a28-b271-2293c5115278@j8g2000yqd.googlegroups.com, "Mark
Lorenzen" <mark.lorenzen@gmail.com> wrote:

> On 11 Aug., 13:38, Ada novice <ycalleecha...@gmx.com> wrote:
>> 
>> Thanks for this information. I'm interested to learn SPARK. If I
>> understand correctly, SPARK aligns itself well with Ada 95 and not yet
>> with Ada 05. Is this because of the strictness of SPARK to provide
>> highly reliable codes and hence it contains only well-tested features
>> (subset of Ada features)? It would be interesting to see some SPARK
>> codes on the wiki page building over time.
> 
> Not quite. SPARK is a proper subset of Ada and is amenable to static
> analysis. This has (in principle) nothing to do with if an Ada feature
> is well-tested or not. You should think of SPARK as a language in its
> own right and not as a subset of some other language.

Why?

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 18:07:51 +0200, Mark Lorenzen  
<mark.lorenzen@gmail.com> a écrit:
> Not quite. SPARK is a proper subset of Ada and is amenable to static
> analysis.
Yes

> This has (in principle) nothing to do with if an Ada feature
> is well-tested or not.
SPARK is actually an Ada subset ;) And it elvoves toward more support of  
this or that Ada feature... while not all, and it will probably never  
support all, this one is true.

> You should think of SPARK as a language in its
> own right and not as a subset of some other language.
 From an abstract point of view, yes. There is SPARK and SPADE, and SPARK  
Examiner is based on SPADE Examiner (if I am not wrong... Rod will correct  
if needed). SPADE mainly came from Pascal, which was the first subsetted.  
But SPARK is still based on Ada. There is SPARK no SPARK Modula, no SPARK  
Oberon and so on.

> Although SPARK
> constantly evolves it will never evolve into a language with the same
> feature-set as Ada - no matter how well tested all Ada festures one
> day will be.
That precisely matter. If some feature are excluded, this is solely  
because they either does not enforce readability (overloading), are not  
predictable enough (while this depend on the state of the art) and could  
be in theory, but not practical or really workable way to do was found (if  
this end up into a SPARK which requires days to validate 10 lines, this is  
not good). Excluded features are excluded for some known reasons, most  
being documented in the SPARK Language Reference Manual.

By the way, the SPARK Language Reference Manual stick to the one Ada : it  
use the same section numbering, naming, and so on.

-- 
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.

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 18:45:33 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> That precisely matter. If some feature are excluded, this is solely  
> because they either does not enforce readability (overloading), are not  
> predictable enough (while this depend on the state of the art)
You may also add some requirements not really expressable in term features  
exclusion, and rather in terms of constructions, like the requirement to  
have a single exit point (multiple return statements are not allowed).  
This kind-of is not a feature matter, this is an execution flow matter.  
This kind of requirements are enforced by the SPARK grammar.


-- 
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.

Re: SPARK code samples

[Ada novice]

Thanks for all the discussions and clarifications guys. If there are
novices like me :) out there wishing to get a simple yet good
introduction to SPARK, I'd recommend this article: "When Computers
Fly, It Has to Be Right: Using SPARK for Flight Control of Small
Unmanned Aerial Vehicles" available at

http://www.stsc.hill.af.mil/crosstalk/2006/09/0609swardgerkencasey.html

YC

Re: SPARK code samples

[Mark Lorenzen]

On 11 Aug., 18:33, "(see below)" <yaldni...@blueyonder.co.uk> wrote:
> On 11/08/2010 17:07, in article
> fa1507ef-77a8-4a28-b271-2293c5115...@j8g2000yqd.googlegroups.com, "Mark
>
> Lorenzen" <mark.loren...@gmail.com> wrote:
> > On 11 Aug., 13:38, Ada novice <ycalleecha...@gmx.com> wrote:
>
> >> Thanks for this information. I'm interested to learn SPARK. If I
> >> understand correctly, SPARK aligns itself well with Ada 95 and not yet
> >> with Ada 05. Is this because of the strictness of SPARK to provide
> >> highly reliable codes and hence it contains only well-tested features
> >> (subset of Ada features)? It would be interesting to see some SPARK
> >> codes on the wiki page building over time.
>
> > Not quite. SPARK is a proper subset of Ada and is amenable to static
> > analysis. This has (in principle) nothing to do with if an Ada feature
> > is well-tested or not. You should think of SPARK as a language in its
> > own right and not as a subset of some other language.
>
> Why?
>
> --
> Bill Findlay
> <surname><forename> chez blueyonder.co.uk

I take it you refer to my last sentence.

First of all because SPARK is not only a set of restrictions imposed
on the Ada language, SPARK also mandates the use of annotations (and
even more so if you want to prove program correctnes). As SPARK
annotations are written as Ada comments, it is true that every SPARK
program is also an Ada program and that may be why people often think
of SPARK as "just" a subset of Ada [1].

I also think there is a risk of getting stuck with SPARK if you try to
design a SPARK program with Ada in mind. You constantly bump into a
useful feature of Ada that is not in SPARK (discriminated types, array
slicing etc.) and you think "why the h... isn't that a part of SPARK
when it's so easy to do in Ada?". So it's probably a way of tuning
your mindset from "Ada with restrictions" into SPARK.

[1] Purists may argue that even with the presence formal annotations,
every SPARK program will be a member of the set of all Ada programs
that include every permutation of every legal comment in every legal
place. Or what?

- Mark L

Re: SPARK code samples

[Dmitry A. Kazakov]

On Wed, 11 Aug 2010 17:26:05 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Wed, 11 Aug 2010 10:44:58 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
>>    http://rosettacode.org/wiki/Main_Page
> I use to see reference to it from place to place. Just have a quick look a  
> few seconds ago. Is it on purpose if all examples seems to lack comments ?  
> I do not see any unsolved task for SPARK.

I suppose it is because the site's maintenance script hasn't yet built the
list. In fact no task is implemented. The list of all tasks is here:

http://rosettacode.org/wiki/Category:Programming_Tasks

(the first 200 (:-))

Pick any you wish.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: SPARK code samples

[Ada novice]

On Aug 11, 7:32 pm, Mark Lorenzen <mark.loren...@gmail.com> wrote:
>
> I also think there is a risk of getting stuck with SPARK if you try to
> design a SPARK program with Ada in mind. You constantly bump into a
> useful feature of Ada that is not in SPARK (discriminated types, array
> slicing etc.) and you think "why the h... isn't that a part of SPARK
> when it's so easy to do in Ada?". So it's probably a way of tuning
> your mindset from "Ada with restrictions" into SPARK.
>

So you're saying not to think in terms of Ada when approaching SPARK?
I have yet to lay my hands on a copy of Barnes' SPARK book to learn
SPARK syntax and I can understand that SPARK is not just Ada with some
annotations.

YC

Re: SPARK code samples

[(see below)]

On 11/08/2010 18:39, in article
bbc93c1c-9e12-4682-912d-9ff961c3a7a5@p7g2000yqa.googlegroups.com, "Ada
novice" <ycalleecharan@gmx.com> wrote:

> On Aug 11, 7:32�pm, Mark Lorenzen <mark.loren...@gmail.com> wrote:
>> 
>> I also think there is a risk of getting stuck with SPARK if you try to
>> design a SPARK program with Ada in mind. You constantly bump into a
>> useful feature of Ada that is not in SPARK (discriminated types, array
>> slicing etc.) and you think "why the h... isn't that a part of SPARK
>> when it's so easy to do in Ada?". So it's probably a way of tuning
>> your mindset from "Ada with restrictions" into SPARK.
>> 
> 
> So you're saying not to think in terms of Ada when approaching SPARK?
> I have yet to lay my hands on a copy of Barnes' SPARK book to learn
> SPARK syntax and I can understand that SPARK is not just Ada with some
> annotations.

Yebbut. It is.

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: SPARK code samples

[Ada novice]

On Aug 11, 7:45 pm, "(see below)" <yaldni...@blueyonder.co.uk> wrote:
> On 11/08/2010 18:39, in article
> bbc93c1c-9e12-4682-912d-9ff961c3a...@p7g2000yqa.googlegroups.com, "Ada
>
> novice" <ycalleecha...@gmx.com> wrote:
> > On Aug 11, 7:32 pm, Mark Lorenzen <mark.loren...@gmail.com> wrote:
>
> >> I also think there is a risk of getting stuck with SPARK if you try to
> >> design a SPARK program with Ada in mind. You constantly bump into a
> >> useful feature of Ada that is not in SPARK (discriminated types, array
> >> slicing etc.) and you think "why the h... isn't that a part of SPARK
> >> when it's so easy to do in Ada?". So it's probably a way of tuning
> >> your mindset from "Ada with restrictions" into SPARK.
>
> > So you're saying not to think in terms of Ada when approaching SPARK?
> > I have yet to lay my hands on a copy of Barnes' SPARK book to learn
> > SPARK syntax and I can understand that SPARK is not just Ada with some
> > annotations.
>
> Yebbut. It is.
>
> --
> Bill Findlay
> <surname><forename> chez blueyonder.co.uk


In this article: "The Exterminators---A small British firm shows that
software bugs aren't inevitable" available at

http://spectrum.ieee.org/computing/software/the-exterminators/0

it is mentioned, I quote: "that the two-step translation--from English
to Z and from Z to Spark--lets engineers keep everything in mind"

I haven't yet personally written any programs in SPARK but does one
has necessarily to understand the Z language in order to use SPARK? I
recall reading somewhere that Barnes's book doesn't discuss the Z
language (I might be wrong though).


Thanks
YC

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 20:00:53 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:
> I haven't yet personally written any programs in SPARK but does one
> has necessarily to understand the Z language in order to use SPARK? I
> recall reading somewhere that Barnes's book doesn't discuss the Z
> language (I might be wrong though).

It is not required (just that if I'm not wrong, SPARK itself was checked  
with Z). Z is one the language/method in this area (some are language,  
some others are language and methods), which are mainly : SPARK, Z, B,  
VDM, ACSL (the latter is special, it targets C :p )

You can use SPARK without knowledge of Z, while this may be interesting if  
you can (I just use to know it a few). This is part of culture. Talking  
about culture, in the domain of logic applied to computer science, you may  
be interested into learning about Intuitionistic Logic (deals with  
constructive proof creation, which talks well to computer science)

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 19:10:22 +0200, Ada novice <ycalleecharan@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.

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov  
<mailbox@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.

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov  
<mailbox@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.

Re: SPARK code samples

[Jeffrey Carter]

>       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@netfront.net ---

Re: SPARK code samples

[cjpsimon]

On 12 août, 04:39, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Wed, 11 Aug 2010 19:33:48 +0200, Dmitry A. Kazakov  
> <mail...@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**15–1.

> 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.

Re: SPARK code samples

[Maciej Sobczak]

On 12 Sie, 04:39, Yannick Duchêne (Hibou57) <yannick_duch...@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

Re: SPARK code samples

[Jacob Sparre Andersen]

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@jacob-sparre.dk
Web-site: http://www.jacob-sparre.dk/

Re: SPARK code samples

[Ada novice]

On Aug 11, 8:21 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Wed, 11 Aug 2010 19:10:22 +0200, Ada novice <ycalleecha...@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

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Thu, 12 Aug 2010 07:02:22 +0200, Jeffrey Carter  
<spam.jrcarter.not@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.

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Thu, 12 Aug 2010 09:29:22 +0200, Maciej Sobczak  
<see.my.homepage@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.

Re: SPARK code samples

[Yannick Duchêne (Hibou57)]

Le Thu, 12 Aug 2010 11:46:04 +0200, Jacob Sparre Andersen <sparre@nbi.dk>  
a écrit:
> I think you have made the problem much too complicated.  Isn't this
> sufficient?  (I haven't got a SPARK Examiner right here.)
> [...]
Agree with this one.
Would you like to post yours ?

Re: SPARK code samples

[Jacob Sparre Andersen]

Yannick Duch�ne wrote:
> Le Thu, 12 Aug 2010 11:46:04 +0200, Jacob Sparre Andersen
> <sparre@nbi.dk> a �crit:

>> I think you have made the problem much too complicated.  Isn't this
>> sufficient?  (I haven't got a SPARK Examiner right here.)

> Agree with this one.
> Would you like to post yours ?

Feel free to post it once you've checked it in SPARK Examiner.

Jacob
-- 
Black Hole: Where the universe made a Divide by Zero.

Re: SPARK code samples

[Phil Thornley]

On 12 Aug, 13:08, Ada novice <ycalleecha...@gmx.com> wrote:
[...]
> 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

If you are using these tutorials with the the latest version of SPARK
(2010) then you might be interested in the updates I've just made to
them for this version.  The biggest change is in the way that function
return annotations are used in the VC generator.

Cheers,

Phil