--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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>