--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie sort specification



You can also have a look at the sorting example in the tutorial:

   http://frama-c.cea.fr/jessie_tutorial_index.html

I know, it is only given "as is" and it needs to be explained, but I 
hope it helps anyway.

- Claude

Virgile Prevosto wrote:
> Hello Kerstin,
> 
> Le mer. 03 juin 2009 13:43:48 CEST,
> "Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit :
> 
>> the array are growing. There's always a problem with the loop 
>> invariants. The post conditions are valid.
> 
> Just a remark here: the post-condition is valid modulo the assumption
> that the loop invariant is valid (if you have a look at the why gui,
> you'll see an hypothesis corresponding to the invariant) and the loop
> test is false (same thing). But this still leaves the issue of proving
> that the loop invariant holds.
> 
>> Is it possible we miss something in the specification? Maybe another loop invariant?
>> It is possible to prove that \forall integer k; 0 <= k < size ==> a[k] ==  k;
> 
> Not with your current loop invariant. Remember that when considering a
> loop, the only thing that jessie knows of all the steps preceding the
> current ones is the loop invariant. Conversely, everything which is not
> stated in the loop invariant is out of reach. In order to complete the
> proof, you'll thus have to add another invariant stating that:
> loop invariant \forall integer k; 0<=k<i ==> a[k] == k;
> (in fact, since this invariant implies that \forall k; 0<=k<i-1 ==>
> a[k]<=a[k+1], the latter becomes useless as a loop invariant).
> 
> Best regards,

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |