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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no 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!postnews.google.com!q22g2000yqm.googlegroups.com!not-for-mail From: Maciej Sobczak Newsgroups: comp.lang.ada Subject: Re: SPARK code samples Date: Thu, 12 Aug 2010 00:29:22 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <1iq8kg021bo4v$.s51i2enx3fzo.dlg@40tude.net> <1lvyv3r0md69x.1cz8ylwiupqva$.dlg@40tude.net> NNTP-Posting-Host: 137.138.182.236 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1281598162 21057 127.0.0.1 (12 Aug 2010 07:29:22 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 12 Aug 2010 07:29:22 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: q22g2000yqm.googlegroups.com; posting-host=137.138.182.236; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.2.6) Gecko/20100625 Firefox/3.6.6,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:13157 Date: 2010-08-12T00:29:22-07:00 List-Id: On 12 Sie, 04:39, Yannick Duch=EAne (Hibou57) wrote: > * I could have made a test to ensure inputs of A and B is in -1000..+1000= , =A0 > while this would not avoid the need to check for the sum validity, as =A0 > formally speaking there is no way to assert anything on Integer range. = =A0 > 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