From: "Peter C. Chapin" <PChapin@vtc.vsc.edu>
Subject: SPARK loop VCs that go "one beyond" the loop?
Date: Sun, 04 Mar 2012 11:11:33 -0500
Date: 2012-03-04T11:11:33-05:00 [thread overview]
Message-ID: <aYCdndGkyL_dCc7S4p2dnAA@giganews.com> (raw)
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 .
next reply other threads:[~2012-03-04 16:11 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-03-04 16:11 Peter C. Chapin [this message]
2012-03-04 18:43 ` SPARK loop VCs that go "one beyond" the loop? Phil Thornley
2012-03-04 19:44 ` Peter C. Chapin
2012-03-06 10:17 ` mark.lorenzen
2012-03-20 18:18 ` Phil Thornley
2012-03-25 10:57 ` Peter C. Chapin
2012-03-25 14:14 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox