--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2015 ---
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.