Re: SPARK: What does it prove?

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 31 May, 02:17, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> 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.

How about using proof abstraction?  Put one set of post-conditions
(for the inefficient version) on the spec and the other set (for the
efficient version) on the body.

Then the post-conditions on the body are proved from the code and the
post-conditions on the spec are proved by a user rule that is
justified by the 'offline' proof of equivalence of the two algorithms.

*** BUT *** the current GPL version (8.1.1) sometimes gets that post-
condition refinement VC wrong.  This only seems to happen when there
is a refined pre and post-condition on the body but no refined state
data, eg for private types, which is where I came across the problem.
(Notified to report@gnat.com on 9th February).

Cheers,

Phil