Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie sort specification

  • Subject: [Frama-c-discuss] Jessie sort specification
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Wed, 3 Jun 2009 14:33:19 +0200
Hello,

 

I've got a question regarding the specification of a very simplified
piece of code, which actually started as a test for proving another more
complex sorting algorithm.

In Jessie different provers we used do not prove that the values in the
array are growing. There's always a problem with the loop invariants.
The post conditions are valid.

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; Does someone know the reason why if this is valid we can't
conclude ==> a[k] <= a[k+1]  ?

 

Very thankful for your advices,

Regards,

 

Kerstin

 

/*@

  requires size >= 0;

  requires \valid_range(a, 0, size-1);

  ensures \forall integer i ;

     0 <= i < size - 1 ==> a[i] <= a[i+1]; */ void wrong_sort(int* a,
int size) {

    int i = 0;

    /*@

        loop invariant 0 <= i <= size;

        loop invariant \forall integer k; 0 <= k < i-1 ==> a[k] <=
a[k+1];

    */

    for(i = 0; i < size; i++)

        a[i] = i;

}

 

 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090603/653036d2/attachment.htm