--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on May 2015 ---
ACSL authors: The ACSL document (1.9) states that having global assigns or ensures statements is equivalent to an additional unnamed behavior: requires P;assigns L;ensures E;behavior B1 ... is equivalent to requires P;behavior <unnamed>?? assumes \true;?? assigns L;?? ensures E;behavior b1 ... [ 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. ] 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?? If so, perhaps the line on p.33 that reads"means that all behaviors given in the contract should be taken into account"should say"means that all named behaviors given in the contract should be taken into account"and similarly for the discussion of 'disjoint behaviors;' - David ? -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150504/cb65b945/attachment.html>