Re: SPARK and integer arithmetic

[Simon Wright <simon@pushface.org>]

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.