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

  • Subject: [Frama-c-discuss] complete/disjoint behaviors and unnamed behaviors
  • From: cok at frontiernet.net (cok at frontiernet.net)
  • Date: Mon, 4 May 2015 19:35:30 +0000 (UTC)
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>