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

[Frama-c-discuss] Specification Examples




Christoph Weber wrote:
> #2: in the second example the preservation of the loop invariant wont work
> 
> 
> 
> /*@ 
>  requires 0 < n;  
>  requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
>  ensures  \forall int k; 0 <= k < n ==> a[k] == b[k];
> */
> void array_cpy(int* a, int n, int* b){ 
>  /*@ loop invariant 0 <= i <= n && \forall int m; 0 <= m < i  ==> a[m] == b[m];
>  */
>  for(int i = 0;i< n;i++){    
>   a[i]=b[i];    
>  } 
> }
> 
> 
> What am I missing, to get the examples running?

You must take into account the fact that arrays a and b might overlap, 
such as if you call array_cpy as

   array_cpy(t,10,t+1);

in such a case your spec does not hold I think.

- Claude

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