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,1d1caf8fb79ff030,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.129.169 with SMTP id nx9mr15290712pbb.2.1330877506241;
        Sun, 04 Mar 2012 08:11:46 -0800 (PST)
Path: 
 h9ni38801pbe.0!nntp.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: Sun, 04 Mar 2012 10:11:43 -0600
Date: Sun, 04 Mar 2012 11:11:33 -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 loop VCs that go "one beyond" the loop?
Message-ID: <aYCdndGkyL_dCc7S4p2dnAA@giganews.com>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-0ZRv+n8IPdM+DRmIbKjlT1750juP8KLT97wcaJC/2ORVZzXu2RynUiy1CWOggNP8KoQvJpPPI3pLAO8!AJdbO+oZ3U/TFBK2Al1XO9X62PAhm0YhI34/gFsOv0gDKKzCzr1/URNpB3yrl/k=
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: 6524
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-03-04T11:11:33-05:00
List-Id: <comp.lang.ada>

It seems like in some cases SPARK tries to prove VCs even under 
"impossible" conditions. In particular when I cut a loop with an 
assertion, SPARK tries to prove that if the assertion is true on one 
pass of the loop it will be true on the next. What if there is no next 
pass? In that case it will try to prove something that isn't true but it 
doesn't matter because that case will never actually arise.

I posted about this problem in 2010 and the solution for the example I 
posted then (and other examples I've since encountered) was to assert 
that certain values don't change during the loop execution... or to just 
work out an entirely different assertion.

I have an example now, however, where I'm running into this problem and 
yet I am unable to see the "trick" to move by it. Below I show 
semi-complete code (still not compilable in the interest of brevity), 
with comments.

First the code. The purpose of the procedure below is to search an array 
of "events" for the first one that matches a given date and then return 
the description of that event. Notice that the description has an 
unconstrained type. Perhaps that is the root of all evil.

procedure Get_Event
   (Date        : in Dates.Date;
    Description : out String;
    Status      : out Status_Type)
--# global in Event_Array;
--# derives Description from Event_Array, Date &
--#         Status      from Event_Array, Date;
is
    I : Event_Index_Type;
begin
    Status      := No_Event;
    Description := (others => ' ');

    I := Event_Index_Type'First;
    loop
       -- Is this item in the event array the one we are looking for?
       if Event_Array(I).Date = Date then

          -- Will its description fit in the available space?
          if Description'Length < Event_Array(I).Description_Size then
             Status := Description_Too_Long;
          else
             for J in Description_Count_Type
                range 1 .. Event_Array(I).Description_Size loop
                --# assert (J - 1) < Description'Length;     -- HERE [1]

                Description(Description'First + (J - 1)) :=  -- HERE [2]
                   Event_Array(I).Description_Text(J);
             end loop;
             Status := Success;
          end if;
          exit;
       end if;

       -- If not, then advance to the next item.
       exit when I = Event_Index_Type'Last;
       I := I + 1;
    end loop;
end Get_Event;

Without the assertion at [1] there is an undischarged VC at [2] related 
to the indexing of Description. The assertion at [1] allows that VC to 
be discharged. Furthermore [1] is proved on loop entry. The problem is 
that the VC from [1] to [1] is undischarged because it tries to show 
that it will remain true even past the last loop iteration. That is, 
SPARK tries to show that if the assertion is true on the last iteration 
it will be true on the next iteration (which never actually occurs). I 
have, of course tinkered with this but so far I haven't hit upon the 
right magic words. I still feel like I'm missing an important principle.

Here is the full VC that is not discharging. Notice that H1 says

    J - 1 < Description'Length

(the Examiner apparently "knows" that String indices start at 1 and so 
Description'Last = Description'Length). The conclusion is trying to show 
that the next value of J will still be in that bound. This is fine 
except for the last iteration... but in that case there is no next value 
of J.

Peter

P.S. I posted a message earlier about discharging a post condition with 
a quantified expression. I just want you (Phil) to know that I read your 
message but I haven't had time to work with that example since. I did 
get an insight about it, however, so I want to reflect on that insight 
for a bit. I'll post again if I have more questions. Thanks for your help!

procedure_get_event_12.
H1:    loop__2__j - 1 < description__index__subtype__1__last .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 64 -> 0 <=
           fld_description_size(element(event_array, [i___1])) and
           fld_description_size(element(event_array, [i___1])) <= 128) .
H3:    for_all(i___2 : integer, 1 <= i___2 and i___2 <= 128 -> 
for_all(i___1 :
           integer, 1 <= i___1 and i___1 <= 64 -> 0 <= element(
           fld_description_text(element(event_array, [i___1])), [i___2]) 
and
           element(fld_description_text(element(event_array, [i___1])), 
[i___2])
           <= 255)) .
H4:    loop__2__j <= 128 .
H5:    loop__2__j >= 1 .
H6:    i__entry__loop__2 >= 1 .
H7:    i__entry__loop__2 <= 64 .
H8:    i >= 1 .
H9:    i <= 64 .
H10:   element(fld_description_text(element(event_array, [i])), 
[loop__2__j])
           >= 0 .
H11:   element(fld_description_text(element(event_array, [i])), 
[loop__2__j])
           <= 255 .
H12:   loop__2__j < fld_description_size(element(event_array, [
           i__entry__loop__2])) .
H13:   integer__size >= 0 .
H14:   character__size >= 0 .
H15:   positive__size >= 0 .
H16:   status_type__size >= 0 .
H17:   description__index__subtype__1__last >= 0 .
H18:   description_index_type__size >= 0 .
H19:   description_count_type__size >= 0 .
H20:   event_record__size >= 0 .
H21:   event_index_type__size >= 0 .
H22:   description__index__subtype__1__last <= 2147483647 .
        ->
C1:    loop__2__j < description__index__subtype__1__last .