From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail From: Stephen Leake Newsgroups: comp.lang.ada Subject: Re: (SPARK Ada) Proving that bitwise and is associative? References: Date: Wed, 30 Apr 2014 02:12:31 -0500 Message-ID: <85k3a7jnog.fsf@stephe-leake.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (windows-nt) Cancel-Lock: sha1:ceHDN8Gxo0WUZ8JYPgHoV85MAtY= MIME-Version: 1.0 Content-Type: text/plain X-Complaints-To: abuse@flashnewsgroups.com Organization: FlashNewsgroups.com X-Trace: dabfc5360a261eef2f4a323673 X-Received-Bytes: 1457 X-Received-Body-CRC: 3205743583 Xref: news.eternal-september.org comp.lang.ada:19621 Date: 2014-04-30T02:12:31-05:00 List-Id: benjaminhocking 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