--- layout: fc_discuss_archives title: Message 13 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



Vergile - thanks for your reply

You are correct of course. I did not mean that the alternative 
desugaring was equivalent, merely that it was an alternate way to 
desugar. One could envision seeing the 'global' assigns and ensures as 
merely a way to factor out of the named behaviors any clauses that were 
common to all of them, rather than as implicitly defining an additional 
behavior.

- David

On 5/5/2015 2:39 AM, Virgile Prevosto wrote:
> Actually, this is true for the ensures clauses, but not for the
> assigns, as adding the global assigns GA to the assigns BA of a
> behavior b
> would mean that when b is active you allow the function to modify both
> GA and BA, leading to a more liberal assigns clause than without GA if
> BA is not a subset (modulo aliasing for added fun) of GA.