* Question about round__ proof function in SPARK proofs.
@ 2011-01-15 17:39 Peter C. Chapin
2011-01-15 18:11 ` Phil Thornley
0 siblings, 1 reply; 3+ messages in thread
From: Peter C. Chapin @ 2011-01-15 17:39 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Question about round__ proof function in SPARK proofs.
2011-01-15 17:39 Question about round__ proof function in SPARK proofs Peter C. Chapin
@ 2011-01-15 18:11 ` Phil Thornley
2011-01-16 13:47 ` Peter C. Chapin
0 siblings, 1 reply; 3+ messages in thread
From: Phil Thornley @ 2011-01-15 18:11 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Question about round__ proof function in SPARK proofs.
2011-01-15 18:11 ` Phil Thornley
@ 2011-01-16 13:47 ` Peter C. Chapin
0 siblings, 0 replies; 3+ messages in thread
From: Peter C. Chapin @ 2011-01-16 13:47 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2011-01-16 13:47 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2011-01-15 17:39 Question about round__ proof function in SPARK proofs Peter C. Chapin
2011-01-15 18:11 ` Phil Thornley
2011-01-16 13:47 ` Peter C. Chapin
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox