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] New Specification Examples

  • Subject: [Frama-c-discuss] New Specification Examples
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue Oct 14 13:17:45 2008
  • In-reply-to: <41A1C9B7510644ABBFFD7ABB57065E88@AHARDPLACE>
  • References: <41A1C9B7510644ABBFFD7ABB57065E88@AHARDPLACE>
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                    |