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

[Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org>]

On 08/14/2010 01:48 PM, Yannick Duchêne (Hibou57) wrote:
> Le Sat, 14 Aug 2010 21:08:43 +0200, Phil Thornley
>>> > For this particular example, I don't understand why you haven't used
>>> > the obvious precondition:
>>> > --# pre A * B in Integer;
>
> But what seems important to me and I would to underline, was also that
> if I did not knew this was possible, this was because it was fr from my
> mind. And this was far from my mind, because looking at it as-is, I
> would have said “what does it prove ? what does it offer ?”. In short,
> this looks like a bad logical interface to me.

It doesn't prove anything, and it's not supposed to. It's a precondition. It 
says, "This precondition must be true for this operation to give correct 
results." It is the caller's duty to meet the precondition.

-- 
Jeff Carter
"To Err is human, to really screw up, you need C++!"
Stéphane Richard
63

--- news://freenews.netfront.net/ - complaints: news@netfront.net ---