--- layout: fc_discuss_archives title: Message 10 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



Hello Claude,

thanks for the pointer to the jessie tutorial.
We were trying to prove the postcondition without "advanced algebraic  
modeling".
The reason for this attempt is a customer that feels a bit overwhelmed  
by inductive definitions.

Do you think it is possible that Jessie can prove a sort algorithm  
that has not been "inductively specified"?

Regards Jens

Am 03.06.2009 um 16:42 schrieb Claude March?:

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