--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on December 2008 ---
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 |