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,f60ad9b53d897d45
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!j25g2000vbs.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Question about round__ proof function in SPARK proofs.
Date: Sat, 15 Jan 2011 10:11:41 -0800 (PST)
Organization: http://groups.google.com
Message-ID: 
 <150284e4-ec97-45ea-b09d-2ed83bfb92c0@j25g2000vbs.googlegroups.com>
References: <Gb6dnSUL7-xIRqzQ4p2dnAA@giganews.com>
NNTP-Posting-Host: 88.97.49.112
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1295115101 9531 127.0.0.1 (15 Jan 2011 18:11:41
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sat, 15 Jan 2011 18:11:41 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: j25g2000vbs.googlegroups.com; posting-host=88.97.49.112;
 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: g2news2.google.com comp.lang.ada:17411
Date: 2011-01-15T10:11:41-08:00
List-Id: <comp.lang.ada>

On Jan 15, 5:39=A0pm, "Peter C. Chapin" <PCha...@vtc.vsc.edu> wrote:
> I'm trying to discharge a VC in a SPARK proof. After simplification I
> have just:
>
> H1: julian_date >=3D 4830771 / 2 .
> H2: julian_date <=3D 2489665 .
>
> The conclusions are:
>
> C1: round__(julian_date + 1 / 2) >=3D - 2147483648 .
> C2: round__(julian_date + 1 / 2) <=3D 2147483647 .
>
> This VC is the result of a type conversion from a floating point type to
> an integer type. It seems evident that the conclusions are true for any
> reasonable definition of round__. I assume the simplifier is not proving
> this VC because it doesn't have any built-in knowledge of the proof
> function round__, even though it was inserted automatically be the
> examiner. So I think maybe I'm supposed to specify the properties of
> round__ somewhere. Am I on track here?

You're quite correct about the round__ function - and the only way to
discharge the VC is to supply user rules that state properties of the
function.

An obvious form for the rule is:

round(1): round__(X) <=3D Y
            may_be_deduced from
        [ X <=3D Y,
          goal(checktype(Y, integer)) ] .

and similarly for the lower bound.

On their own these rules probably aren't going to work for this VC
(although it's worth a try) because there isn't a direct match for the
X<=3DY sidecondition.  Adding a preceding check annotation might do the
trick:

--# check (julian_date + 0.5) in Integer;

Cheers,

Phil