From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b36bbdc1595d0665 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news4.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!138.195.8.3.MISMATCH!news.ecp.fr!news.jacob-sparre.dk!pnx.dk!not-for-mail From: Jacob Sparre Andersen Newsgroups: comp.lang.ada Subject: Re: SPARK code samples Date: Thu, 12 Aug 2010 11:46:04 +0200 Organization: Jacob Sparre Andersen Message-ID: <87bp98rwo3.fsf@hugsarin.sparre-andersen.dk> References: <1iq8kg021bo4v$.s51i2enx3fzo.dlg@40tude.net> <1lvyv3r0md69x.1cz8ylwiupqva$.dlg@40tude.net> NNTP-Posting-Host: 95.209.236.21.bredband.3.dk Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Trace: munin.nbi.dk 1281606372 9166 95.209.236.21 (12 Aug 2010 09:46:12 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 12 Aug 2010 09:46:12 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (gnu/linux) Cancel-Lock: sha1:CNV2hbEV0OZF1TWmZ8bquzJpVc8= Xref: g2news1.google.com comp.lang.ada:13166 Date: 2010-08-12T11:46:04+02:00 List-Id: 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/