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.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,8bc4790fae14ac33,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.224.10.6 with SMTP id n6mr8240256qan.4.1366407233844;
        Fri, 19 Apr 2013 14:33:53 -0700 (PDT)
X-Received: by 10.49.72.225 with SMTP id g1mr1776568qev.36.1366407233830; Fri,
 19 Apr 2013 14:33:53 -0700 (PDT)
Path: 
 ef9ni2qab.0!nntp.google.com!gp5no3187343qab.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 19 Apr 2013 14:33:53 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=46.171.80.166;
 posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 46.171.80.166
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <957ef6e4-23d8-499f-ba19-20d32e82a7df@googlegroups.com>
Subject: SPARK - divide algorithm issue
From: Maciej Sobczak <see.my.homepage@gmail.com>
Injection-Date: Fri, 19 Apr 2013 21:33:53 +0000
Content-Type: text/plain; charset=ISO-8859-1
Date: 2013-04-19T14:33:53-07:00
List-Id: <comp.lang.ada>

Playing further with implementing division in SPARK, but this time an example from John Barnes book is causing problems:

    procedure Divide (M, N : in Integer; Q, R : out Integer);
    --# derives Q, R from M, N;
    --# pre M >= 0 and N > 0;
    --# post (M = Q * N + R) and (R < N) and R >= 0;

    procedure Divide (M, N : in Integer; Q, R : out Integer) is
    begin
        Q := 0;
        R := M;
        loop
            --# assert M = Q * N + R and R >= 0;
            exit when R < N;
            Q := Q + 1;   -- here
            R := R - N;
        end loop;
    end Divide;

In this example SPARK cannot prove that the marked line (Q := Q + 1) is safe with respect to Integer'Last. What is most frustrating is that this is a book example, where it is claimed to verify OK.
Is it possible that in the meantime there were changes in the toolchain that caused this to stop working?
If yes, what would be the proper strategy to hint the prover that the loop will never run longer than the range of positive values?

(This example looks nicer with Natural and Positive types used where appropriate, but I wanted to make it as close to the original as possible.)

Again, this is SPARK GPL 2011.

-- 
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com