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!feeder.eternal-september.org!news.szaf.org!news.enyo.de!.POSTED!not-for-mail
From: Florian Weimer <fw@deneb.enyo.de>
Newsgroups: comp.lang.ada
Subject: Re: SPARK and integer arithmetic
Date: Mon, 03 Oct 2016 17:39:08 +0200
Message-ID: <87mvil1lyb.fsf@mid.deneb.enyo.de>
References: <87poo1a57p.fsf@mid.deneb.enyo.de>
	<0d01480e-ddd4-4746-99ad-4f1e6adab436@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
X-Trace: news.enyo.de 1475509148 17115 192.168.18.20 (3 Oct 2016 15:39:08 GMT)
X-Complaints-To: news@enyo.de
Cancel-Lock: sha1:hKpDzoI1RARbIxcpTSWDAW+m3vM=
Xref: news.eternal-september.org comp.lang.ada:31976
Date: 2016-10-03T17:39:08+02:00
List-Id: <comp.lang.ada>

* Mark Lorenzen:

> On Sunday, September 18, 2016 at 12:10:36 PM UTC+2, Florian Weimer wrote:
>> I'm trying to find out the capabilities of the SPARK when it comes to
>> verifying the correctness of integer arithmetic (and absence of
>> constraint errors).
>> 
>> The Barnes book (in the 2006 edition) is not really that helpful.  I'm
>> not even using the current SPARK tools, but the SPARK 2012 GPL
>> edition, but the command line options still are different from those
>> described in the book.
>
> I would really like to advice you to use the latest SPARK GPL toolset
> and the SPARK book
>
> https://www.amazon.co.uk/Building-High-Integrity-Applications-Spark/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1475489273&sr=8-1&keywords=high+integrity+applications
>
> The new SPARK language and toolset are major improvements over the old ones.

Indeed, but they do not cover this particular issue well (proving
correctness of wraparound arithmetic).