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

[Frama-c-discuss] behaviors in ACSL




Hi,

Although the contract, as it is written, is (probably) satisfied by the 
code. I'd like to emphasize that this is probably not the right way to 
write it. The general advice is

      *always think in priority from the client side*

in other words, when some client code calls

   r = find_array(a, l, v)

then what info would be useful to get ? I think what is useful in that 
case is

  depending on the value r returned :

    if r = l then I learn that forall integer k; 0 <= k < l ==> a[k] != v

    if r < l then I learn that a[r] == v and
                    forall integer k; 0 <= k < r ==>  a[k] != v

To get exactly this info, the contract should be written as

behavior match:
    ensures \result < length ==>
       a[\result] == value &&
       \forall integer k; 0 <= k < \result ==>  a[k] != value;

behavior no_match:
    ensures \result == length ==>
	\forall integer k; 0 <= k < length ==> a[k] != value;

the assumes clause should be used for other purposes: see binary_search 
example from ACSL document.

- Claude

Pascal Cuoq wrote:
> Hi!
> 
> I am cc-ing the mailing list.
> 
>> /*@
>>   requires 0 <= length;
>>   requires \valid_range(a, 0, length-1);
>>
>>   assigns nothing;
>>
>>   behavior match:
>>     assumes \exists integer k; 0 <= k < length ==> a[k] == value;
>>     ensures \result < length ==> a[\result] == value;
>>     ensures \forall integer k; 0 <= k < \result ==>  a[k] != value;
>>
>>   behavior no_match:
>>     assumes \forall integer k; 0 <= k < length ==> a[k] != value;
>>     ensures \result == length;
>>
>>   complete behaviors;
>>   disjoint behaviors;
>>
>>  */
>>  int find_array (int* a, int length, int value);
-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |