Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: Re: [Frama-c-discuss] Une nouvelle semaine avec nouveaux problèmes
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Mon Oct 20 13:18:24 2008
  • In-reply-to: <4920C83E850E461B9C49CE429FE46013@AHARDPLACE>
  • References: <4920C83E850E461B9C49CE429FE46013@AHARDPLACE>
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