Re: SPARK understand me very well... me neither

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

Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> So I would much prefer the simple and obvious version of the
> precondition and code to be the version on Rosetta Code so that anyone
> browsing that site for information about SPARK doesn't get a wrong
> view of the language.
Updated with this added comment :

> Note: how do you ensure then “A * B in Natural” ? Either with
> a proof prior to Multiply invokation or using another form
> of Multiply where input A and B would be restricted to a range
> which ensures the resulting product is always valid. Exemple :
>    type Input_Type is range 0 .. 10;
>    type Result_Type is range 0 .. 100;
> and had a version of Multiply using these types.
> On the other hand, if arguments of Multiply are constants, this
> is provable straight away.

I wanted to add this comment, because the How is of a practicable  
importance.


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