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

[Frama-c-discuss] New Specification Examples



I have a hard time to follow each iteration in this example, but I would 
like to emphasize a fundamental mistake here.

Christoph Weber wrote:
> /*@
>  requires last >= first;
>  requires \valid_range(first, 0, last-first-1);
>  behavior is_not_empty:  
>   assumes last > first;
>   ensures  \forall integer i; 0 <= i < last-first ==> first [i] == value;
>  behavior is_empty:
>   assumes last == first;
>   ensures last == first; 
>  
> */
> void fill_int_array (int* first, int* last,  int value ) {
 > ...
 > }

> In this example the ensurance of the postcondition does not work due to the changing value of first.

Wrong, from the caller point of view, parameters (like first and last) 
do not change (there are not modifiable lvalues)

Consequently, any use of \old on them like in \old(first) is useless. 
Also, the ensures clause last==first in behavior is_empty is a 
triviality (from the assumes clause)

Hope this helps,

-- 
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                    |