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] axiomatic "function"

  • Subject: [Frama-c-discuss] axiomatic "function"
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Fri, 23 Jan 2009 13:10:23 +0100
Hello,

some days ago, I committed an algorithm "unique_copy".

After some corrections, the algorithm was proven. But to position of the incrementation was modified.

I restored the original algorithm and adapted the loop invariants:

My problem is now, that a VC fails to proof and I have no Idea why.

I would like you to have a look and tell me, what needs to be corrected.

=====================

/*@ axiomatic Specification_unique_copy {

    logic integer spec_unique_copy{La,Lb}(int* a, integer i, int* b, integer j);

    axiom unique_copy_empty{La,Lb}:
     \forall int* a, int* b, integer i, j;
     0 > i || 0 > j ==> spec_unique_copy{La,Lb}(a, i, b, j) == 0;

  axiom unique_copy_first_element{La,Lb}:
     \forall int* a, int* b, integer i, j;
     0 == i ==>
     spec_unique_copy{La,Lb}(a, i, b, j) ==
     spec_unique_copy{La,Lb}(a, i-1, b, j-1) + 1;

    axiom unique_copy_equal{La,Lb}:
     \forall int* a, int* b, integer i, j;
     0 < i &&
     \at(a[i],La) == \at(a[i-1],La) ==>
     spec_unique_copy{La,Lb}(a, i, b, j) ==
     spec_unique_copy{La,Lb}(a, i-1, b, j);

     axiom unique_copy_not_equal{La,Lb}:
     \forall int* a, int* b, integer i, j;
     0 < i && 0 <= j &&
     (\at(a[i],La) != \at(a[i-1],La) <==> \at(a[i],La) == \at(b[j],Lb)) ==>
     spec_unique_copy{La,Lb}(a, i, b, j) ==
     spec_unique_copy{La,Lb}(a, i-1, b, j-1) + 1;


  axiom unique_copy_not_equal_label{La,Lb1,Lb2}:
     \forall int* a, int* b, integer i, j;
     (\forall integer i; 0<= i <= j ==>
        \at(b[i],Lb1) == \at(b[i],Lb2)) ==>
     spec_unique_copy{La,Lb1}(a, i, b, j) ==
     spec_unique_copy{La,Lb2}(a, i, b, j);
   }

*/
/*@
    predicate disjoint_arrays(int* a, int* b, integer n) =
        \forall integer i, k;
            0 <= i < n && 0 <= k < n ==> a + i != b + k;
*/

/*@
     requires 0 <= length;
     requires \valid_range(a, 0, length-1);
     requires \valid_range(b, 0, length-1);
     requires disjoint_arrays(a,b,length);
     

  ensures 0 <= \result <= length;
  ensures \result == spec_unique_copy{Old,Here}(a, length-1, b, \result-1);
*/
int unique_copy_array(int* a, int length, int* b)
{

    int i = 0;
    int j = 0;

    if (length == 0)
        return j; 
    int value = a[i];
    b[j] = value; 
     
    /*@
   loop invariant 0 <= i < length;
   loop invariant j <= i;
   loop invariant 0 <= j < length;
   loop invariant a[i] == value;
   loop invariant b[j] == value ;

   loop invariant j == spec_unique_copy{Pre,Here}(a, i-1, b, j-1);   
     */
    while (++i != length)
    { 
        if (!(value == a[i]))
        {
            value = a[i];            
            b[++j] = value;
           
            /*@ assert
               a[i] != a[i-1] ==> b[j] != b[j-1]; 
          */
   
            /*@ assert
               j+1 == spec_unique_copy{Pre,Here}(a, i, b, j);
            */                  
        }
        
    }
    return ++j;
}
==========

I would also like to know, why adding following requirement will cause loop invariants to fail:

requires disjoint_arrays(a, b, length);


Cheers

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090123/cc293c17/attachment.htm