Re: SPARK: What does it prove?

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

Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> It is common to talk about SPARK proofs but of course what the  
> Simplifier is
> actually proving are the verification conditions generated by the  
> Examiner.
> Formally this leaves open the question of if those verification  
> conditions
> have anything to do with reality or not.
The question, “what does it prove ?”, raise another corollary question,  
which is “what can it says ?” or “what can it talks about ?”.

I'm currently trying to make proofs on some binary stuffs, which has  
always seems obvious to me, and at the time of trying to prove it, I see I  
can't even prove the third of the initial postcondition I wanted my  
functions to have, because there are some I can't prove at all (I'm not  
talking about RTC, rather about postcondition expressing properties, and  
it is far less easy than proving RTC conditions).

If is funny to note that these difficulty are a consequence of SPARK tied  
to Ada. An example : Ada has modular type, but can't see modular types has  
polynomials, and the relevant modal, which could help, would be this one :  
polynomial. Has Ada don't has this, SPARK doesn't too.

Another things also : sometime, it is better to make proof on an abstract  
algorithm, which not efficient, and it is too much difficult to the same  
proof (prove postconditions from preconditions and the algorithm) with the  
efficient version. However, it would be more easy to demonstrate than the  
efficient algorithm is an equivalent transformation of the more abstract  
non-efficient one.

I mean, prove something on function F, demonstrate function G is  
equivalent to function F, so as legally assert the postconditions of F are  
also prove on G, because there was on F and G is equivalent to F.

This is another kind of thing SPARK cannot express or talk/say about.

This may be the start of some answers to the question “what can it proves  
?” or “what can't it proves ?”, which are similar questions.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.