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

[Frama-c-discuss] axiomatic "function"



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