Re: SPARK code samples

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.