* SPARK loop VCs that go "one beyond" the loop?
@ 2012-03-04 16:11 Peter C. Chapin
2012-03-04 18:43 ` Phil Thornley
0 siblings, 1 reply; 7+ messages in thread
From: Peter C. Chapin @ 2012-03-04 16:11 UTC (permalink / 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 .
^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: SPARK loop VCs that go "one beyond" the loop?
2012-03-04 16:11 SPARK loop VCs that go "one beyond" the loop? Peter C. Chapin
@ 2012-03-04 18:43 ` Phil Thornley
2012-03-04 19:44 ` Peter C. Chapin
0 siblings, 1 reply; 7+ messages in thread
From: Phil Thornley @ 2012-03-04 18:43 UTC (permalink / raw)
In article <aYCdndGkyL_dCc7S4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu
says...
[...snipped...]
Peter,
I would like to give a more considered reply than I have time for just
now, however:
I am fairly sure that what you need to add to the assertion is the
result of the earlier check:
Event_Array(I).Description_Size <= Description'Length
You may also need to state that the upper bound on J is not changed by
the loop body:
Event_Array = Event_Array%
Cheers,
Phil
> 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!
If there's too much code to post to news then feel free to mail it to me
- the address is on the sparksure web site if you don't still have it.
^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: SPARK loop VCs that go "one beyond" the loop?
2012-03-04 18:43 ` Phil Thornley
@ 2012-03-04 19:44 ` Peter C. Chapin
2012-03-06 10:17 ` mark.lorenzen
2012-03-20 18:18 ` Phil Thornley
0 siblings, 2 replies; 7+ messages in thread
From: Peter C. Chapin @ 2012-03-04 19:44 UTC (permalink / raw)
On 2012-03-04 13:43, Phil Thornley wrote:
> I would like to give a more considered reply than I have time for just
> now, however:
>
> I am fairly sure that what you need to add to the assertion is the
> result of the earlier check:
> Event_Array(I).Description_Size<= Description'Length
>
> You may also need to state that the upper bound on J is not changed by
> the loop body:
> Event_Array = Event_Array%
I tried changing the assertion to
--# assert Event_Array(I).Description_Size <= Description'Length and
--# (J - 1) < Description'Length;
but that didn't help by itself. When I tried adding Event_Array =
Event_Array% that didn't seem to do anything. I have a feeling that
because Event_Array has mode 'in' the Examiner is already considering
its constancy.
I did notice, however, that there was a hypothesis that talked about
Event_Array(i__loop__2__entry). It seemed to me that the hypothesis was
somewhat related to my conclusion so as a guess I tried
--# assert Event_Array(I).Description_Size <= Description'Length and
--# I = I% and
--# (J - 1) < Description'Length;
That worked! However, I'm still trying to understand the general
principle that can guide me in these situations. I feel like I have to
resort to semi-random attempts until I stumble into something that works.
Anyway, thanks for your hint.
Peter
^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: SPARK loop VCs that go "one beyond" the loop?
2012-03-04 19:44 ` Peter C. Chapin
@ 2012-03-06 10:17 ` mark.lorenzen
2012-03-20 18:18 ` Phil Thornley
1 sibling, 0 replies; 7+ messages in thread
From: mark.lorenzen @ 2012-03-06 10:17 UTC (permalink / raw)
Den søndag den 4. marts 2012 20.44.41 UTC+1 skrev Peter C. Chapin:
>
> That worked! However, I'm still trying to understand the general
> principle that can guide me in these situations. I feel like I have to
> resort to semi-random attempts until I stumble into something that works.
Peter,
I strongly recommend Phil's proof tutorials that can be found here: http://www.sparksure.com/7.html
Try and have a look at chapters 7 and 8 in order to understand how the examiner transforms loop constructs into a standard form, from which it generates VCs. This should help you understand where invariants can be placed and what they should express.
Regards,
Mark L
^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: SPARK loop VCs that go "one beyond" the loop?
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
1 sibling, 1 reply; 7+ messages in thread
From: Phil Thornley @ 2012-03-20 18:18 UTC (permalink / raw)
In article <vpqdnYMbkompW87S4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu
says...
[snip]
> I did notice, however, that there was a hypothesis that talked about
> Event_Array(i__loop__2__entry). It seemed to me that the hypothesis was
> somewhat related to my conclusion so as a guess I tried
>
> --# assert Event_Array(I).Description_Size <= Description'Length and --# I
> = I% and --# (J - 1) < Description'Length;
>
> That worked! However, I'm still trying to understand the general principle
> that can guide me in these situations. I feel like I have to resort to
> semi-random attempts until I stumble into something that works.
Peter,
The clue to the fact that you needed to add I=I% is in the hypotheses.
I put enough code around the code in your initial post to get the VC that
you also posted.
Then, with the additional condition, there are two particular hypotheses:
H2: fld_description_size(element(event_array, [i])) <=
description__index__subtype__1__last .
H13: loop__2__j < fld_description_size(element(event_array, [
i__entry__loop__2])) .
where the conclusion is:
C1: loop__2__j < description__index__subtype__1__last .
so by including I=I% in the loop invariant (which becomes i=i__entry__loop__2
in the VC) the conclusion is provable.
Cheers,
Phil
(You may well think that the way that VCs are presented makes it very
difficult to spot this sort of thing. If this VC is read by VC_View then it
becomes:
For path(s) from assertion of line 72 to assertion of line 72
H1: A - 1 < B__last .
H2: fld_description_size(element(event_array, [i])) <= B__last .
H5: A <= 128 .
H6: A >= 1 .
H11: element(fld_description_text(element(event_array, [i])), [A]) >= 0 .
H12: element(fld_description_text(element(event_array, [i])), [A]) <= 255 .
H13: A < fld_description_size(element(event_array, [i__entry__loop__2])) .
H22: B__last >= 0 .
H23: B__last <= 2147483647 .
C1: A < B__last .
A = loop__2__j
B__last = description__index__subtype__1__last
which makes it a bit easier to spot.)
^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: SPARK loop VCs that go "one beyond" the loop?
2012-03-20 18:18 ` Phil Thornley
@ 2012-03-25 10:57 ` Peter C. Chapin
2012-03-25 14:14 ` Phil Thornley
0 siblings, 1 reply; 7+ messages in thread
From: Peter C. Chapin @ 2012-03-25 10:57 UTC (permalink / raw)
On 2012-03-20 14:18, Phil Thornley wrote:
> Peter,
>
> The clue to the fact that you needed to add I=I% is in the hypotheses.
>
> I put enough code around the code in your initial post to get the VC that
> you also posted.
>
> Then, with the additional condition, there are two particular hypotheses:
> H2: fld_description_size(element(event_array, [i]))<=
> description__index__subtype__1__last .
> H13: loop__2__j< fld_description_size(element(event_array, [
> i__entry__loop__2])) .
> where the conclusion is:
> C1: loop__2__j< description__index__subtype__1__last .
>
> so by including I=I% in the loop invariant (which becomes i=i__entry__loop__2
> in the VC) the conclusion is provable.
Thanks for your comments. They are helpful, as always. The problem I'm
having, in general (no longer related to any specific VC), is that if
the loop assertion mentions the loop index variable there is a tendency
for SPARK to generate an unprovable VC of the form
Hx: loop__1__i <= some_array__index__subtype__1__last
...
Cy: loop__1__i + 1 <= some_array__index__subtype__1__last
This is for the path from the assertion to the assertion and it's trying
to show that the loop index variable is always in bounds of some
array... even *after* the last iteration. This generally isn't true, but
it doesn't matter because there is no "next" iteration in that case.
If I write a loop assertion that doesn't mention the loop index variable
this problem doesn't arise, naturally. However, I can avoid it anyway by
doing... something... with that loop assertion. My problem is that I
haven't quite figured out what triggers VCs like the one above so I have
to kind of guess my way around how to avoid them.
Peter
^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: SPARK loop VCs that go "one beyond" the loop?
2012-03-25 10:57 ` Peter C. Chapin
@ 2012-03-25 14:14 ` Phil Thornley
0 siblings, 0 replies; 7+ messages in thread
From: Phil Thornley @ 2012-03-25 14:14 UTC (permalink / raw)
In article <YridnaJ19_2RZ_PS4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu
says...
> Thanks for your comments. They are helpful, as always. The problem I'm
> having, in general (no longer related to any specific VC), is that if
> the loop assertion mentions the loop index variable there is a tendency
> for SPARK to generate an unprovable VC of the form
>
> Hx: loop__1__i <= some_array__index__subtype__1__last
> ...
> Cy: loop__1__i + 1 <= some_array__index__subtype__1__last
>
> This is for the path from the assertion to the assertion and it's trying
> to show that the loop index variable is always in bounds of some
> array... even *after* the last iteration. This generally isn't true, but
> it doesn't matter because there is no "next" iteration in that case.
>
> If I write a loop assertion that doesn't mention the loop index variable
> this problem doesn't arise, naturally. However, I can avoid it anyway by
> doing... something... with that loop assertion. My problem is that I
> haven't quite figured out what triggers VCs like the one above so I have
> to kind of guess my way around how to avoid them.
I don't believe that the Examiner generates a path *to* the loop
iteration for the last iteration - I can only imagine that there is
something you are not seeing.
It's quite true that any VC that references the loop index will have
your Hx above - because the loop index is within the bounds of its
subtype at the start of the path.
However, for all paths from the assertion to the assertion, the Examiner
will certainly generate a hypothesis that the loop index is strictly
less than the final value of the loop range (assuming absence of
'reverse' of course).
Therefore you have to look at what you know about the relative values of
the last loop index value and 'Last of the array index subtype.
This is one part of what was required for the code in in your original
post (Event_Array(I).Description_Size <= Description'Length) and you
provided the other part.
This undoubtedly gets more involved when the last loop index value is an
expression referencing one or more variables, but this shouldn't make
any fundamental difference. (In this case it's sometimes helpful to
temporarily introduce a local variable for the upper bound of the loop
range.)
Cheers,
Phil
^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2012-03-25 14:14 UTC | newest]
Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-03-04 16:11 SPARK loop VCs that go "one beyond" the loop? Peter C. Chapin
2012-03-04 18:43 ` 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
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox