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: SPARK and integer arithmetic
Date: Sun, 18 Sep 2016 12:10:34 +0200
Message-ID: <87poo1a57p.fsf@mid.deneb.enyo.de>
Mime-Version: 1.0
Content-Type: text/plain
X-Trace: news.enyo.de 1474193434 10346 192.168.18.20 (18 Sep 2016 10:10:34
 GMT)
X-Complaints-To: news@enyo.de
Cancel-Lock: sha1:lMfvenSi0ghCacofaAVlBr7ZCmw=
Xref: news.eternal-september.org comp.lang.ada:31805
Date: 2016-09-18T12:10:34+02:00
List-Id: <comp.lang.ada>

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.

The warm-up exercise goes like this:

   package Sum is
      
      function Add (A, B : Integer) return Integer;
      --# pre 0 <= A and A <= 10 and 0 <= B and B <= 10;
      --# return A + B;
      
   end Sum;
   
   package body Sum is
      
      function Add (A, B : Integer) return Integer is
      begin
         return A + B;
      end Add;
      
   end Sum;

The SPARK configuration file contains:

   package Standard is
      type Integer is range -2147483648 .. 2147483647;
   end Standard;
   
I found the -vcg option, which causes spark the generate a sum/add.vcg
file, which shows that there is something to prove.  The sum/add.rls
contains the type range information from the configuration file.

Running sparksimp outputs:

   /home/fw/tmp/ada/arith/sum/add.vcg
      *** ERROR - The Simplifier failed.

The exit status is still zero, but I assume that this means that the
required proofs could not be performed.  Is this because the built-in
prover is not sufficiently powerful, or is there something else I can
do here (such as using an external prover)?