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

Re: [Frama-c-discuss] Une nouvelle semaine avec nouveaux problèmes



Hi Christoph,

eine neue Woche bringt neue Antworten
(according to Google Translate ...)

Is there, or will there be a possibility to include requirement clauses in
> behavior statements?
>
>
I am quite happy that you ask! Indeed, I asked for the introduction of
requirements into behaviors, and they painfully made their way to ACSL
documentation, but not yet to implementation. I do not know if they will be
part of the next release.

Referring to the assigns clause:
> Will assigns \nothing ensure that nothing has been altered?
>

almost. It ensures that all global variables and memory locations that (1)
were allocated in the pre-state and (2) do not belong to the set of assigned
globals and memory locations have the same value in the post-state than in
the pre-state. This does not prevent their value from being modified during
the call and then restored.


> And will assigns <something> ensure that nothing else has been altered?
>

with the same meaning as before, yes.


> Would using the assigns statement make the label \at(...,Pre) in a complete
> copy spec obsolete?
>

in fact, \at(..,Pre) in a postcondition will not be allowed anymore. It
should be written \at(...,Old) or \old(...).
Assigns can only replace the kind of value-preserving postconditions that
read like [ensures v == \old(v)]. In this case, it is much better to write
an assigns clause for modularity: you only specify what changes. Otherwise,
\old(...) is still very useful to refer to the value of something in the
pre-state.

>
> Using the assigns statement I will encounter an other problem. Following
> example:
>
> /*@
>  requires 0 < n;
>  requires \valid_range(a, 0, n-1);
>  assigns  a[0..n - 1];
>  ensures  \forall integer i; 0 <= i < n ==> a[i] == 0;
> */
> void array_zero(int* a, int n)
> {
>
>     /*@
>    loop invariant 0 <= i <= n;
>    loop invariant \forall integer k; 0 <= k < i ==> a[k] == 0;
>    loop assigns i, a[0..i-1];
>     */
>     for (int i = 0; i < n; i++)
>     {
>         a[i] = 0;
>     }
> }
> If I put a assings clause in the function contract and use  a loop in the
> function I cannot hold the postcondition. I think it might has something to
> to with preserving it like a loop invariant. In the 1_3 manual I discovered
> the loop assigns but I don't know how to use it. (what is the upper bound
> and will I need to use quantifiers?)
>

 Your example is correct. The problem is that the Jessie plugin currently
does not support loop assigns, but it is on top of our todo list. In
particular, i-1 is the proper upper bound, indeed at loop entry you have
assigned nothing, which can be written a[0..-1] and after each loop you
increase this bound. Hopefully you can verify this example with the next
release!

HTH
-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/28a8675b/attachment.htm