--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on October 2008 ---
Hi, in anticipation of extended behavior handling I rethought my examples in Order to reach a more complete specification. I need to know some things: Is there, or will there be a possibility to include requirement clauses in behavior statements? I would like to include the cases is_empty and is_not_empty. Therefore I have to extend following spec to include zero-length arrays: /*@ requires last > first; requires disjoint_arrays(first, result, last-first); requires \valid_range (first, 0, last-first-1); requires \valid_range (result, 0, last-first-1); ensures \forall integer i; 0 <= i < last-first ==> result[i] == first[i]; */ int* copy_int_array (int* first, int* last, int* result); altered to: /*@ requires last >= first; requires disjoint_arrays(first, result, last-first); behavior is_empty: assumes last > first; requires \valid_range (first, 0, last-first-1); requires \valid_range (result, 0, last-first-1); assigns first[0..last-first-1]; ensures \forall integer i; 0 <= i < last-first ==> result[i] == first[i]; behavior is_not_empty: assumes last == first; assigns \nothing; */ int* copy_int_array (int* first, int* last, int* result); Referring to the assigns clause: Will assigns \nothing ensure that nothing has been altered? And will assigns <something> ensure that nothing else has been altered? Would using the assigns statement make the label \at(...,Pre) in a complete copy spec obsolete? Using the assigns statement I will encounter an other problem. Following example: /*@ requires 0 < n; requires \valid_range(a, 0, n-1); assigns a[0..n - 1]; ensures \forall integer i; 0 <= i < n ==> a[i] == 0; */ void array_zero(int* a, int n) { /*@ loop invariant 0 <= i <= n; loop invariant \forall integer k; 0 <= k < i ==> a[k] == 0; loop assigns i, a[0..i-1]; */ for (int i = 0; i < n; i++) { a[i] = 0; } } If I put a assings clause in the function contract and use a loop in the function I cannot hold the postcondition. I think it might has something to to with preserving it like a loop invariant. In the 1_3 manual I discovered the loop assigns but I don't know how to use it. (what is the upper bound and will I need to use quantifiers?) Well that's it, I guess. Merci d'avance Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/d97746cf/attachment.htm