--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2008 ---
Hello again, today I would like to post some observations I made, as well as ask about a specification example ========================================================= 1. I have a copy algorithm in the array-notation supported by jessie. /*@ requires 0 <= length; requires disjoint_arrays(a, dest, length); requires \valid_range (a, 0, length-1); requires \valid_range (dest, 0, length-1); //assigns dest[0..length]; ensures \forall integer i; 0 <= i < length ==> dest[i] == \old(a[i]); */ int copy_array (int* a, int length, int* dest) { int index_a = 0; int index_dest = 0; /*@ loop invariant 0 <= index_a <= length; loop invariant index_dest == index_a; loop invariant 0 <= index_dest <= length; loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == dest[k]; loop assigns dest[0 .. index_dest]; */ while (index_a != length) { dest[index_dest++] = a[index_a++]; } return index_dest; } The statement of interrest is: assigns dest[0..length]; while the loop assigns works, i wont get a green bullet for the postcondition. ========================================================= 2. In an other Algorithm, I discovered a second Problem. /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); requires \valid_range (dest, 0, length-1); requires disjoint_arrays(a, dest, length-1); ensures \forall integer k; 0 <= k < \result ==> dest[k] != value; ensures \result == length - nb_occ{Old}(a, 0, length, value); */ int remove_copy_array (int* a, int length, int* dest, int value ) { int index_a = 0; int index_dest = 0; /*@ loop invariant 0 <= index_a <= length; loop invariant index_dest <= index_a; loop invariant 0 <= index_dest <= length; loop invariant \forall integer k; 0 <= k < index_dest ==> dest[k] != value; loop invariant index_dest == index_a - nb_occ{Pre}(a, 0, index_a, value); */ for ( ; index_a != length; ++index_a) if (!(a[index_a] == value)) { dest[index_dest] = a[index_a]; ++index_dest; } return index_dest; } a. On my opinion it is a little confusing to use the Pre-Label in the loop and the Old-Label and meaning the same state. b. The loop invariant/ensures-clause using the nb_occ does not yet work. I tried to define it with incrementing steps and decrementing steps. /*@ axiomatic NbOcc { logic integer nb_occ{L}(int* a, integer index, integer length, int value); axiom nb_occ_empty{L}: \forall int* a, int value, integer index, length; index >= length ==> nb_occ(a,index,length,value) == 0; axiom nb_occ_true{L}: \forall int* a, int value, integer index, length; index < length && a[index] == value ==> nb_occ(a,index,length,value) == nb_occ(a,index+1,length,value) + 1; axiom nb_occ_false{L}: \forall int* a, int value, integer index, length; index < length && a[index] != value ==> nb_occ(a,index,length,value) == nb_occ(a,index+1,length,value); } */ I dont see why it wont work. ========================================================= 3. I would like to see an alternative description of \valid_range: The documentation describes it as: \valid_range(p; i; j) := \offset_min(p) <= i ^ \offset_max(p) >= j; I would like to know, wheter the one_past_the_end_pointer is included or not. And if it is included, does it make much sense to include it in the specification of a function. Well, I am grateful for help Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081208/3bd0e217/attachment.htm