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

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

Le Sat, 14 Aug 2010 23:50:08 +0200, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:
> 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.
I understand that objection ; but in the mean time, isn't it the purpose  
of an interface to ease use and to help to manage things ? The  
precondition is part of the interface as much as the function signature is  
after all.

I will need some time to try an imagine new approachs.

The one I was using until now was more looking mathematical proof (by the  
way, the same kind of you may have with VDM or something of the like),  
that is a step by step hypothesis -> conclusion -> new hypothesis -> new  
conclusion, each possibly referring to previous conclusions. That is the  
reason why I oftenly number each step and refer to these in conclusions as  
“... -- from (x) and (y)” where x and y are numbers of previous steps.  
Indeed, this approach does not seems to be well suited with SPARK and ends  
into unsolvable things. The fact it does not only validate proof, but also  
tries to prove things it-self is an important fact with consequences. This  
is not really a validator, this is half validator and half automatic  
prover. And this impacts the way it works. You cannot expect it to follow  
your step-by-step proof (because it may use this or that hypothesis its  
own way, possibly going into long backtrackings or explorations), and you  
cannot expect it to prove every things automatically (that point is  
obvious). This makes it unfamiliar to me, so I will have to figure some  
other ways to do with it.

Will have some opportunities, as I would like to test it on some other  
Rosetta examples (along with some personal uses I am planning and already  
started to test).