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:
> Yannick, I realise that you are an enthusiast for this but it's not
> the way that the job is done in practice - it doesn't scale up for
> real problems.  When it takes seven proof statements to (fail to)
> prove a simple multiplication then this method isn't practicable for
> the sorts of expressions that appear in the real-world models of
> embedded systems.

That is precisely the matter I was wondering about. It appears all my  
attempt always end to be too much complicated.

> So we shouldn't be publicising this approach in sites such as Rossetta
> Code.
OK.


> For this particular example, I don't understand why you haven't used
> the obvious precondition:
> --# pre A * B in Integer;
Because I did not knew this was feasible. May be due to a background: I  
use to write less or more formal comment in Pascal or Ada source, to show  
that this and that was valid or how this could be valid. So all my attempt  
so far was focusing on the How Be Valid (and though SPARK was working this  
way also). If i understand you, there is a more declarative approach. Is  
that it ?

> The version of the precondition that will work best (measured by
> leaving the lowest number of unproven VCs) depends on how the calling
> code ensures that it meets the precondition.
This is one of the reason I am thinking about the How Be Valid. Balancing  
your way and the (not so good) way I used so far, I would say one says  
How, the other does not.

> The easiest way to achieve this (for general purpose functions like
> Multiply) is by having the subtypes of the parameters as constrained
> as possible, so, as long as the bounds on the two terms are small
> enough, meeting this simpler version of the precondition is
> automatic.
Yes. That is exactly what I had in a Pascal application I remember of. I  
had a kind of screen area, and I had to be sure the area could always be  
computed without overflow. I defined a type for area, and a type for  
height and width, so that the maximum of width and height could never  
commit an overflow and area could always be computed in any case. This fat  
more simple to check for that checking less constrained width and height  
would not commit an overflow.

The reason why I did not used it here, is because I did not see a  
legitimate way to restrict the input type beside of the result type.

> OTOH, if the bounds of the parameter subtypes can't ensure the
> precondition, then the program has to use a defensive check, in which
> case your version of the precondition may work better (if the
> defensive check is exactly that precondition).
That is the case where input cannot be constrained, which is, if this has  
to be fully general and generic. While the way I exposed with the Pascal  
example above, is better whenever possible.

> In a well-designed program, the subtype constraints should match the
> usage of the variables of the subtypes
Agree, except that I could not see a way to restrict here.

> 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.
That is the target and the reason why I posted the question here. Hopfully  
I get the good anwser.

Wish I had read such a reply priorly, this would have save me lot of  
headache.

Will try to revisit all my approach with this ideas in mind.

Hope you are not too much tired with my beginner's questions.

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