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=-0.3 required=5.0 tests=BAYES_00,FREEMAIL_FROM,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,d144bcd39fd2a06b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.66.72.131 with SMTP id d3mr6293504pav.38.1356812778621;
        Sat, 29 Dec 2012 12:26:18 -0800 (PST)
Path: 
 6ni71216pbd.1!nntp.google.com!border1.nntp.dca.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newspeer1.nac.net!news.mi.ras.ru!spln!extra.newsguy.com!feeds.phibee-telecom.net!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader03.nrc01.news.zen.net.uk.POSTED!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Constraint_Error from arithmetic operations
Date: Thu, 27 Dec 2012 10:33:00 -0000
Message-ID: <MPG.2b46340f43edd90398969f@news.zen.co.uk>
References: <87r4mbrgl8.fsf@mid.deneb.enyo.de>
Reply-To: phil.jpthornley@gmail.com
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: 13135c7b.news.zen.co.uk
X-Trace: 
 DXC=JRM0hI4M[4D0`W9<OnKcIMf2FgniPJjgB=dR0\ckLKG@WeZ<[7LZNRF8EblaVK`U]EUhLi?]0KG=K8a@D]61DD8HGUK\SEnB<7A
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-12-27T10:33:00+00:00
List-Id: <comp.lang.ada>

In article <87r4mbrgl8.fsf@mid.deneb.enyo.de>, fw@deneb.enyo.de says...
> 
> 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.
> 
(The publication dates of the three SPARK books are 1997, 2003, and 2012 
so I'm not sure which one you mean).

I don't know how you read the any of books to get that understanding, 
but SPARK has always included the option to generate overflow checks 
(and they are now always included whenever VCs are generated).

With this code:

======================================
package P
is

   type My_Int is new Short_Integer range -20_000 .. 20_000;
   --  Short_Integer is -32768 .. 32767.

   function Op (A, B : My_Int) return My_Int;

end P;


package body P
is

   function Op (A, B : My_Int) return My_Int
   is
   begin
      return (A + B) / 2;
   end Op;

end P;
======================================

There is an unprovable VC remaining after simplification:

function_op_1.
H1:    a >= - 20000 .
H2:    a <= 20000 .
H3:    b >= - 20000 .
H4:    b <= 20000 .
H5:    my_int__size >= 0 .
       ->
C1:    a + b >= - 32768 .
C2:    a + b <= 32767 .

which comes from the overflow check on the plus operation in the return 
expression.

(You have to specify the ranges for Short_Integer of course - this is in 
the configuration file for the particular compiler you are using).

Originally the base range had to be specified using a 'base type 
assertion' but the recent versions of the language have included the use 
of derived types, as above.

Cheers,

Phil