From: benjaminhocking <benjaminhocking@gmail.com>
Subject: (SPARK Ada) Proving that bitwise and is associative?
Date: Tue, 29 Apr 2014 10:59:41 -0500
Date: 2014-04-29T10:59:41-05:00 [thread overview]
Message-ID: <nd2dnZa1N-bwUcLOnZ2dnUVZ_gOdnZ2d@giganews.com> (raw)
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?
next reply other threads:[~2014-04-29 15:59 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-04-29 15:59 benjaminhocking [this message]
2014-04-29 19:11 ` (SPARK Ada) Proving that bitwise and is associative? benjaminhocking
2014-04-30 12:39 ` Phil Thornley
2014-04-30 7:12 ` Stephen Leake
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox