From: "Peter C. Chapin" <PChapin@vtc.vsc.edu>
Subject: Re: Question about round__ proof function in SPARK proofs.
Date: Sun, 16 Jan 2011 08:47:10 -0500
Date: 2011-01-16T08:47:10-05:00 [thread overview]
Message-ID: <V86dncJcGcZ8a6_QRVn_vwA@giganews.com> (raw)
In-Reply-To: <150284e4-ec97-45ea-b09d-2ed83bfb92c0@j25g2000vbs.googlegroups.com>
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
prev parent reply other threads:[~2011-01-16 13:47 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
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 message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox