Re: SPARK code samples

[Maciej Sobczak <see.my.homepage@gmail.com>]

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