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

[Phil Thornley <phil.jpthornley@gmail.com>]

On 14 Aug, 17:44, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley  
> <phil.jpthorn...@gmail.com> a écrit:
[...]
> > 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.
OK - that seems a pretty good reason :-)

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

For a general purpose function such as this the author can't define
sensible subtypes for the individual inputs because the condition that
the function relies on is itself a function of both of the inputs.
That's why there has to be a precondition.  The job of the author is
always to come up with the weakest precondition that does the job.

For the Multiply function the weakest possible precondition is the
condition that Multiply requires - that the product of the two actual
parameters is a valid Integer.

[...]
> Hope you are not too much tired with my beginner's questions.
Not a problem - and it's one of the functions of c.l.a to provide a
forum for such questions.  (You'll know when I get tired of answering
because I'll stop :-)

Cheers,

Phil