From: "Peter C. Chapin" <PChapin@vtc.vsc.edu>
Subject: Question about round__ proof function in SPARK proofs.
Date: Sat, 15 Jan 2011 12:39:15 -0500
Date: 2011-01-15T12:39:15-05:00 [thread overview]
Message-ID: <Gb6dnSUL7-xIRqzQ4p2dnAA@giganews.com> (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
next reply other threads:[~2011-01-15 17:39 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-01-15 17:39 Peter C. Chapin [this message]
2011-01-15 18:11 ` Question about round__ proof function in SPARK proofs Phil Thornley
2011-01-16 13:47 ` Peter C. Chapin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox