Re: Lost in translation (with SPARK user rules)

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

Le Wed, 26 May 2010 21:32:02 +0200, Pascal Obry <pascal@obry.net> a écrit:
> Right. I think the response to this is pragmatism and cost. For non
> critical softwares do you think it is reasonable to use SPARK? This is
> only a matter of trade-off I think.
So, depends on how it is balanced.

If the component of an application of an application, is to be executed  
thousand of times in a day or in a week, and especially if this is to be  
executed automatically, the trade-off should give weight to verifiability,  
even for applications which are not know to be critical in the usual sense.

For others, I would say proofs could help to understand why it works (not  
just how). This could be nice for pedagogy, as a formal comments is always  
more readable than implicit human language (not that I don't like the  
latter, just that it is sometime too much weak). And for maintainability,  
like modifying this and that for more efficiency, or simply adding a  
functionality, with the insurance nothing will be broken on the way.

What kind of trade-off should not care ?

(note: I was thinking about also some other reasons, however not exposed,  
to be short)

> [...] where data are read from the same socket but
> two consecutive read won't return the same value. There is way in SPARK
> to deal with that, to avoid SPARK complaining that you have ineffective
> code... not straight forward!
>
> Pascal.
I see what the subject was looking like


I was thinking about something. With my attempted pre/post/check in mind,  
I was reading the SPARK source, and noticed one thing : the postconditions  
in the SPARK sources, are far less detailed than what I was attempting to  
do with my packages. To be honest, I was not only to prove there will not  
be any runtime error, I was also using postconditions to express  
properties and logics. So obviously, this ends in much more difficult  
complicated things to demonstrate.

This may be a rule of thumb with SPARK : first, try to have a program  
proved to be runtime error free, then after only, when that done, try to  
add more to express logic properties.

May be I was somewhere between proof of absence of runtime error and data  
refinement (I mean what in french is named « réification »). Possibly  
SPARK do not the best with the latter. Finally, stating a procedure or  
function has this and that logic property, is another way to state this is  
the concrete implementation of the abstraction which has these same  
properties ; so this is refinement/reification.

Perhaps SPARK can do that... a bit, and perhaps I was wrong to expect it  
could fully do that.

So this rule of thumb : start with proof of no runtime error first, and  
only later try more and don't expect this is required to succeed ?

However, being able to add rules which could be applied the same way  
embedded rules are, would really be nice. While I suspect this would not  
be compatible with some efficiency requirements of the SPARK Simplifier  
(if only I could build the Simplifier from modified source, but I can't).


-- 
There is even better than a pragma Assert: a SPARK --# check.