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]

[Frama-c-discuss] complete/disjoint behaviors and unnamed behaviors

Hello,

2015-05-04 21:35 GMT+02:00 cok at frontiernet.net <cok at frontiernet.net>:
> The ACSL document (1.9) states that having global assigns or ensures
> statements is equivalent to an additional unnamed behavior:

> [ An alternative desugaring, for example, would be to not introduce a new
> unnamed behavior when there are named behaviors, but rather add the global
> assigns and ensures into every named behavior. ]

Actually, this is true for the ensures clauses, but not for the
assigns, as adding the global assigns GA to the assigns BA of a
behavior b
would mean that when b is active you allow the function to modify both
GA and BA, leading to a more liberal assigns clause than without GA if
BA is not a subset (modulo aliasing for added fun) of GA.

>
> Also
>
> complete behaviors;
>
> is defined as the assertion that the disjunction of all the assumes clauses
> of the contract's behaviors is true.
>
> This would appear to include the assumes clause of the unnamed behavior, but
> that would make the 'complete behaviors' assertion a tautology. Similarly,
> the 'disjoint behaviors' assertion would always be a contradiction.
> Or do you intend that these are syntactic sugar for a list of the **named**
> behaviors only?
>

Thanks for your feedback. You're right of course, complete behaviors
and disjoint behaviors only concern named behaviors. We'll change the
manual according to your suggestion in the next version of the manual.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile