--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] jessie questions



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