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

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>