From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,6d79efdb8dde2c5a
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!postnews.google.com!k10g2000yqa.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
Date: Sun, 15 Aug 2010 21:58:20 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <846423d1-82e8-4bb8-87a9-e667c20e8c16@k10g2000yqa.googlegroups.com>
References: <op.vhguffh3ule2fv@garhos>
 <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com>
 <i49oif$1c85$1@adenine.netfront.net> <op.vhh3bwnwxmjfy8@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1281934700 781 127.0.0.1 (16 Aug 2010 04:58:20
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 16 Aug 2010 04:58:20 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: k10g2000yqa.googlegroups.com; posting-host=80.177.171.182;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:13384
Date: 2010-08-15T21:58:20-07:00
List-Id: <comp.lang.ada>

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

> There is no Magic here, what you do not have in Check annotations, you =
=A0
> hide it in user rules. The reason why I do not like it, is because you do=
 =A0
> not see the proofs any more (or great part of it are missing), this is no=
t =A0
> any more part of the source. Proofs should come with the implementation. =
I =A0
> 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 >=3D 2*X, so (X + Y) div 2 >=3D X.
---------------------------------------------------------*/
binary_search_rule(1): (X + Y) div 2 >=3D X
                         may_be_deduced_from
                       [ X <=3D Y,
                         X >=3D 1,
                         Y >=3D 1] .

/*---------------------------------------------------------
-- Rule 2:
--   Justification:
--     X + Y <=3D 2*Y, so (X + Y) div 2 <=3D Y.
---------------------------------------------------------*/
binary_search_rule(2): (X + Y) div 2 <=3D Y
                         may_be_deduced_from
                       [ X <=3D Y,
                         X >=3D 1,
                         Y >=3D 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 <=3D y .
H2:   x >=3D 1 .
H3:   y >=3D 1 .
     ->
C1:   (x + y) div 2 >=3D x .
C2:   (x + y) div 2 <=3D 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