Question about round__ proof function in SPARK proofs.

Question about round__ proof function in SPARK proofs.

[Peter C. Chapin]

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?

Thanks in advance for any insights you might have.

Peter

Re: Question about round__ proof function in SPARK proofs.

[Phil Thornley]

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

Re: Question about round__ proof function in SPARK proofs.

[Peter C. Chapin]

On 2011-01-15 13:11, Phil Thornley wrote:

> 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.

Thanks so much for your suggestions. I'll try it out at my first
opportunity. If I run into any other problems I'll be sure to post here
again :)

Peter