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=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,b0cbdc5a85122130,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.204.154.143 with SMTP id o15mr48708bkw.4.1330524496634;
        Wed, 29 Feb 2012 06:08:16 -0800 (PST)
Path: 
 t13ni83628bkb.0!nntp.google.com!news1.google.com!news2.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 29 Feb 2012 08:08:16 -0600
Date: Wed, 29 Feb 2012 09:08:16 -0500
From: "Peter C. Chapin" <PChapin@vtc.vsc.edu>
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64;
 rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: SPARK question: discharging post-conditions.
Message-ID: <HcWdne5sWI7NrNPS4p2dnAA@giganews.com>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-mb63GtjmZTPF1wR+ydVwExZVbDll7x5r2s9/q4EBIxfR9CFKEas+vYTU8E0zsQMXRBWDKykAXunoJV1!8Ae9HyNLgId1sh4E5szm+TEckOYBMrG5guhul+ugOOASAwUGJBPq4imhZNno5T4=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2825
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-02-29T09:08:16-05:00
List-Id: <comp.lang.ada>

I'm experimenting with a small exercise and it's not working quite like 
I expected. I could show my real code, but in the interest or brevity 
I'll try to show the structure and hope that's enough to address my issue.

I'm writing a simple sorting procedure that consists of a main loop. 
Something like (not compilable):

procedure Sort(Buffer : in out Buffer_Type) is
begin
   for I in Index_Type range X .. Y loop
     -- Do interesting stuff...

     --# assert [that the array is partially sorted]
   end loop;
end Sort;

Notice that the assertion is at the bottom of the loop. I'm wondering if 
that's a problem for me. The idea is that the first time through the 
loop the assertion will be true. Furthermore if the assertion is true on 
one pass it will be true on the next. This is fine. In fact, the VCs 
associated with the assertion are proving (they are universally 
quantified expressions and I'm using alt-ergo to deal with them; the 
SPARK simplifier doesn't prove them).

My problem is that the post-condition, which says that the array is 
fully sorted, isn't being discharged. When I look at the post condition, 
the hypotheses are rather trivial. They basically say that the first two 
elements are in order and, oh yeah, every element of the array is in the 
range of its subtype. That's it. Naturally that's not enough to prove 
the conclusion.

My question is: why isn't the information in the loop assertion making 
it to the post-condition? The path quoted for the VC is "from assertion 
of line [the assert I show above] to finish." Yet the asserted condition 
is not mentioned in the VC's hypotheses.

I think I'm misunderstanding something, but I don't recall this coming 
up for me before.

Thanks!

Peter