Re: SPARK : third example for Roesetta - reviewers welcome

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

On 15 Aug, 23:27, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:

> There is no Magic here, what you do not have in Check annotations, you  
> hide it in user rules. The reason why I do not like it, is because you do  
> not see the proofs any more (or great part of it are missing), this is not  
> any more part of the source. Proofs should come with the implementation. I  
> cannot dissociate both.

User rules are as formal or as informal as you choose to make them.

In my version of this example I have some user rules with informal
justifications - eg:
/*---------------------------------------------------------
-- Rule 1:
--   Justification:
--     X + Y >= 2*X, so (X + Y) div 2 >= X.
---------------------------------------------------------*/
binary_search_rule(1): (X + Y) div 2 >= X
                         may_be_deduced_from
                       [ X <= Y,
                         X >= 1,
                         Y >= 1] .

/*---------------------------------------------------------
-- Rule 2:
--   Justification:
--     X + Y <= 2*Y, so (X + Y) div 2 <= Y.
---------------------------------------------------------*/
binary_search_rule(2): (X + Y) div 2 <= Y
                         may_be_deduced_from
                       [ X <= Y,
                         X >= 1,
                         Y >= 1] .

if you need more formality then first define a couple of integer
variables x and y in a .fdl file:

title procedure search_rules:

   var x, y : integer;

end;

then prove the following VC using the Proof Checker:

search_rules_1.
H1:   x <= y .
H2:   x >= 1 .
H3:   y >= 1 .
     ->
C1:   (x + y) div 2 >= x .
C2:   (x + y) div 2 <= y .

The only manual step in this is the translation of the rule to the VC
- and so long as you use the same names with just the case changed (X -
> x) and layout the VC similarly to the rule this step is very easy to
validate manually.

Cheers,

Phil