From: Stephen Leake <stephen_leake@stephe-leake.org>
Subject: Re: (SPARK Ada) Proving that bitwise and is associative?
Date: Wed, 30 Apr 2014 02:12:31 -0500
Date: 2014-04-30T02:12:31-05:00 [thread overview]
Message-ID: <85k3a7jnog.fsf@stephe-leake.org> (raw)
In-Reply-To: nd2dnZa1N-bwUcLOnZ2dnUVZ_gOdnZ2d@giganews.com
benjaminhocking <benjaminhocking@gmail.com> writes:
> I have the following check statements embedded in some SPARK Ada code:
> --# check (value and (mask_32 and Unsigned_32'Mod(LMask_8))) = 0;
> --# check ((value and mask_32) and Unsigned_32'Mod(LMask_8)) = 0;
> The SPARK examiner is able to prove the first one (using inference)
> but not the second one, even though it has already proven the first
> one, so should be able to prove it by using the first one combined
> with the fact that bitwise and is associative. Does anyone have any
> suggestions for how I can help it?
I have no experience with SPARK, but would it not be more efficient to
assert somewhere that bitwise "and" is associative, rather than checking
it indirectly here?
--
-- Stephe
prev parent reply other threads:[~2014-04-30 7:12 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-04-29 15:59 (SPARK Ada) Proving that bitwise and is associative? benjaminhocking
2014-04-29 19:11 ` benjaminhocking
2014-04-30 12:39 ` Phil Thornley
2014-04-30 7:12 ` Stephen Leake [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