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 (Kerstin Hartig)
  • Date: Wed, 3 Jun 2009 13:43:48 +0200


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,


  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;