--- layout: fc_discuss_archives title: Message 89 from Frama-C-discuss on October 2008 ---
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