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

[Frama-c-discuss] Specification Examples



Hello,

I'm exercising with the jessie-tool learn the usage of the ACSL-Language.
I have two examples. My Problem is with the second one.

#1: works fine, i get green bullets
/*@ 
 requires 0 < n;  
 requires \valid_range(a, 0, n-1);
 ensures  \forall int i; 0 <= i < n ==> a[i] == 0;
*/
void array_zero(int* a, int n){ 
 /*@ loop invariant 0 <= i <= n && \forall int k; 0 <= k < i ==> a[k] == 0; 
 */
 for(int i = 0;i< n;i++){
  a[i]=0;
 } 
}

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

Christoph


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081009/7620ab3b/attachment.htm