SPARK question: discharging post-conditions.

SPARK question: discharging post-conditions.

[Peter C. Chapin]

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

Re: SPARK question: discharging post-conditions.

[Phil Thornley]

In article <HcWdne5sWI7NrNPS4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...
> 
> 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.

That shouldn't be a problem at all.  The only requirement is that every 
path over the loop that does not exit the loop must meet an assertion 
somewhere.

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

I'm not sure exactly what you mean here - do you mean a postcondition 
that you have stated for the procedure or the conclusions on the VCs 
that are generated by the Examiner for the "For path(s) ... to finish" 
VCs?

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

Any VC that is generated for a path starting from an assertion will 
(certainly "should") have hypotheses for the assertion.

Are you looking at the VC generated by the Examiner (in the .vcg file) 
or a version of the VC that has been processed by one or more provers.

If the latter then these tools have an unfortunate tendency to remove 
any hypothesis that they can reduce to True (since it clearly adds 
nothing to the rest of the hypotheses).

Another reason for a prover removing a hypothesis is if it can show that 
it has no possible connection with any conclusion. If the values 
referenced in a hypothesis cannot be connected to any value in a 
conclusion via any other hypothesis then it might well be removed.

To be any more definite we need to see the actual code, I'm afraid.

Cheers,

Phil