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=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,d144bcd39fd2a06b,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.180.86.201 with SMTP id r9mr9866671wiz.4.1356837414436;
        Sat, 29 Dec 2012 19:16:54 -0800 (PST)
Path: 
 i11ni337243wiw.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.131.MISMATCH!xlned.com!feeder3.xlned.com!news.astraweb.com!border6.a.newsrouter.astraweb.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!feeder.erje.net!eu.feeder.erje.net!news.szaf.org!news.gnuher.de!news.enyo.de!.POSTED!not-for-mail
From: Florian Weimer <fw@deneb.enyo.de>
Newsgroups: comp.lang.ada
Subject: Constraint_Error from arithmetic operations
Date: Thu, 27 Dec 2012 10:26:27 +0100
Message-ID: <87r4mbrgl8.fsf@mid.deneb.enyo.de>
Mime-Version: 1.0
X-Trace: news.enyo.de 1356600386 27850 172.17.135.6 (27 Dec 2012 09:26:26 GMT)
X-Complaints-To: news@enyo.de
Cancel-Lock: sha1:qrwXXEOmE1vfA983X8UFUoouxBw=
Content-Type: text/plain; charset=us-ascii
Date: 2012-12-27T10:26:27+01:00
List-Id: <comp.lang.ada>

This is somewhat related to the recent discussion on exception
contracts, but I'm more interested in what can be right now (with
current tools).

I recently browsed through Barnes' 2006 SPARK book and noticed that
SPARK has a rather drastic approach to arithmetic operations which
overflow and fail to deliver the mathematically correct result
(program termination).  The SPARK tools do not seem to be able to
statically show that arithmetic operators do not overflow, which is
obviously difficult in the general case, but should be doable with
help from the programmer.

Eventually, I hope to be able to show that protocol decoders do not
trigger arithmetic overflow due to sufficient manual checking.  (It
does not matter if this checking is actually dead code, or if the
checks are somewhat conservative, they just need to be there.)
Checking for the absence of Constraint_Error from indexed components
would be a bonus.