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

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

Le Sat, 14 Aug 2010 21:08:43 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
>> 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 :-)
If you feel so, nothing bad so :)

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.

Well, as said, the case is special here : an example posted at Rosetta,  
and this have special requirements.

But if this was for a real project, I am pretty sure I would have insisted  
to go on with a pre-condition which would have offered something  
(something to help the client of the function to setup a valid context or  
to prove a given invokation context is valid). As-is, I feel this simply  
discharge all of the proof responsibility on the client side. That is why  
this kind of idea was very far from my mind. Otherwise, about the use of "  
... in Type_Name" in a Check or Assert SPARK annotation, this is thing  
already done multiple me for me. This was just in the particular context,  
the one of a --# pre annonation, I've never imagine this could be an  
option.

By the way, that is true the proof may become very complex (at least  
relatively compared to the function is applies to). But it goes with proof  
as it goes with implementation : once done, this is done and you can invok  
the method/function as many time as you want.

The pre-condition also may seems complex too. But this may be valuable, or  
be a better logical interface in the long run, if this help the clients to  
figure out how and when the function may be legitimately used. That is the  
purpose of an interface after all.

I do not mean I desagree with you here, I just do not want to focus too  
much on that “I did not knew it was possible” which is mostly anecdotal  
here. The reason why I did not had this alternative in mind is far more  
important.

I feel we understand each other on this point any way. Just wanted to  
makes it explicit.

I have also opened a thread on fr.comp.lang.ada based on this experience  
and your valuable comments, just to get more opportunity to have talks  
about “The Art and the Way to do”, as I feel there are far too much few  
about it :( (I mean, not enough talks and experiences testimony about  
SPARK).

Have a nice day! :)


Yannick