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!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: SPARK and integer arithmetic
Date: Sun, 18 Sep 2016 16:37:44 +0100
Organization: A noiseless patient Spider
Message-ID: <lyy42p1anr.fsf@pushface.org>
References: <87poo1a57p.fsf@mid.deneb.enyo.de>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="869b0aa788dd1f334f900d4a63ead7ae";
	logging-data="22582"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX197aJ3AJA9RE3fOE0nGqui2VhBkQQ/rtfA="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.5 (darwin)
Cancel-Lock: sha1:8y08pcoPnPMmzSk2XN2tiXCXZOs=
	sha1:0UIuDZCSPXeCF7GQdUMVRWJUs+o=
Xref: news.eternal-september.org comp.lang.ada:31806
Date: 2016-09-18T16:37:44+01:00
List-Id: <comp.lang.ada>

Florian Weimer <fw@deneb.enyo.de> writes:

> 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.

With SPARK 2016 GPL, which of course uses different syntax, the
correctness of this piece of arithmetic is indeed verified.

package Sum
with SPARK_Mode
is

   function Add (A, B : Integer) return Integer
   with
     Pre => (A in 0 .. 10) and (B in 0 .. 10),
     Post => Add'Result = A + B;

end Sum;

package body Sum
with SPARK_Mode
is

   function Add (A, B : Integer) return Integer is
   begin
      return A - B;                              -- note the error!
   end Add;

end Sum;

$ gnatprove -P sum
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
sum.ads:8:14: medium: postcondition might fail, cannot prove Add'Result = A + B (e.g. when A = 0 and Add'Result = -1 and B = 1)

(I'm surprised gnatprove is so tentative!)

The proof succeeds with the proper operator.