From: "Peter C. Chapin" <PChapin@vtc.vsc.edu>
Subject: SPARK question: discharging post-conditions.
Date: Wed, 29 Feb 2012 09:08:16 -0500
Date: 2012-02-29T09:08:16-05:00 [thread overview]
Message-ID: <HcWdne5sWI7NrNPS4p2dnAA@giganews.com> (raw)
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
next reply other threads:[~2012-02-29 14:08 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-02-29 14:08 Peter C. Chapin [this message]
2012-02-29 17:14 ` SPARK question: discharging post-conditions 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