Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] behaviors in ACSL

  • Subject: [Frama-c-discuss] behaviors in ACSL
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Thu, 11 Dec 2008 13:02:24 +0100
  • In-reply-to: <B31C9971-A1EF-4C74-92DC-C131D05069FB@cea.fr>
  • References: <4FA912B7D4D8468FBACF5B5DDE198385@AHARDPLACE> <C88F4E451E884829944B1A79F874868C@AHARDPLACE> <20081010124942.4f8a52db@is005115> <1B3FA18004D74D5787DB01AD1EB95900@AHARDPLACE> <14791e30810100413p41eb2e81i89e9f8da63b3040d@mail.gmail.com> <C5F22AF6BA75453CA2EDEADB270E33F3@AHARDPLACE> <14791e30810100505i22345288s5a519d7eab160828@mail.gmail.com> <8F56F47622DB4469B4EBD734D7C08712@AHARDPLACE> <48F33637.5080109@inria.fr> <756435F7D0F44C23B2C7F91E053F77B9@AHARDPLACE> <14791e30810140214r29c903b5w3287a3c33afde56f@mail.gmail.com> <0215081F-3BED-430D-9C3B-E5ABD4212D94@first.fraunhofer.de> <8CFD89A5-CBA1-4F9A-BA19-7ACDDC6F47A4@cea.fr> <A1761223-6344-4BF1-865F-C9F808F931EE@first.fraunhofer.de> <6B884929-2B22-48C2-AC51-44A1AD02D93A@cea.fr> <FA587957-6A90-415F-971C-21781A0AB522@first.fraunhofer.de> <B31C9971-A1EF-4C74-92DC-C131D05069FB@cea.fr>

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                    |