SPARK loop VCs that go "one beyond" the loop?

SPARK loop VCs that go "one beyond" the loop?

[Peter C. Chapin]

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 .

Re: SPARK loop VCs that go "one beyond" the loop?

[Phil Thornley]

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.

Re: SPARK loop VCs that go "one beyond" the loop?

[Peter C. Chapin]

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

Re: SPARK loop VCs that go "one beyond" the loop?

[mark.lorenzen]

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

Re: SPARK loop VCs that go "one beyond" the loop?

[Phil Thornley]

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.)

Re: SPARK loop VCs that go "one beyond" the loop?

[Peter C. Chapin]

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

Re: SPARK loop VCs that go "one beyond" the loop?

[Phil Thornley]

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