Re: Question about round__ proof function in SPARK proofs.

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

On Jan 15, 5:39 pm, "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 >= 4830771 / 2 .
> H2: julian_date <= 2489665 .
>
> The conclusions are:
>
> C1: round__(julian_date + 1 / 2) >= - 2147483648 .
> C2: round__(julian_date + 1 / 2) <= 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) <= Y
            may_be_deduced from
        [ X <= 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<=Y sidecondition.  Adding a preceding check annotation might do the
trick:

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

Cheers,

Phil