--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2015 ---
Thanks for these (correct) observations. Frama-C properly interprets the complete and disjoint clauses, as you can check by using ?frama-c -print? or ?frama-c-gui?. For instance, having named behaviors X and Y, 'complete behaviors? means ?complete behaviors X,Y?, thus excluding the default un-named behavior. Note also that it is possible ? and highly recommended ? to list the behavior names in such clauses, and have many of them. Example: behavior A: assumes x >= 0 ; behavior B: assumes x <= 0 ; behavior C: assumes y >= 0 ; behavior D: assumes y < 0 ; behavior E: assumes x >= 0 && y >= 0 ; complete behaviors A,B ; complete behaviors C,D ; complete behaviors B,D,E ; // not disjoint disjoint behaviors C,D ; disjoint behaviors D,E ; // not complete For deductive proofs, we plan to have in WP the possibility to make a case-split on a call by considering one of the available complete-behaviors clause, depending on the context. There surely exists other interesting features to consider that makes use of complete and disjoint clauses. L. > Le 4 mai 2015 ? 21:35, cok at frontiernet.net a ?crit : > > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150505/ca135778/attachment-0001.html>