--- layout: fc_discuss_archives title: Message 44 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:
> Hi and a thank you for the help,
> 
> but I like to continue questioning where I stopped.
> 
> You remember the array_cpy:
> /*@
>  requires 0 < n;
>  requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1)&& disjoint_arrays(a, b, n);
>  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];
>     }
> }
> 
> This works fine with the Hydrogen-version on Win 32 and the Z3 prover. On the Helium edition on OSX it terminates successfully with CVC3 (Z3 not aviable). Now I'd like to know:
> - what has to be done or added to let ergo v0.8 or simplify verify it as well.

You have to improve ergo and simplify :-)

One advice is to use "integer" instead of ints in your annotations:

ensures  \forall integer k; 0 <= k < n ==> a[k] == b[k];

and so on.

> - array_cpy is only partial specified on my opinion the ensures clause has to be altered to
>     ensures  \forall int k; 0 <= k < n ==> a[k] == \old(b[k]);
> using this I receive an error due to preservation of loop invariant. I think  the comparison in the loop invariant has to be altered to 
>      a[m] == \at(b[m],Old);
> but FramaC will return
>     File array_test.c, line 28, characters 80-93:
>     Error during analysis of annotation: logic label `Old' not found
>     array_test.c:29: Warning: ignoring logic loop annotation
> I tried a bit but I where unable to cheat my way around.

Old does not mean anything in loop invariants. You have to use Pre:
a[m] == \at(b[m],Pre)