--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on February 2011 ---
Le mer. 16 f?vr. 2011 17:49:10 CET, "Boris Hollas" <hollas at informatik.htw-dresden.de> a ?crit : > so, if ACSL predicates are evaluated by-value, is there a way to define a > predicate that has the same behavior as > > #define unchanged(k) (k <==> \old(k)) > > that can be used in other contracts? No, this is not possible. \at and \old cannot be expressed as normal ACSL functions. > > Alternatively, I may use assigns L instead and make sure that k is not in > L. But there's a problem if the function contains an if-statement and > assigns k in one branch, but not in the other. Since assigns is a keyword > like requires or ensures, I can't specify a postcondition such as > > ensures (cond ==> assigns k) && (!cond ==> assigns \empty); > > It is possible using behaviors but these can't be specified as predicates > to be reused in other contracts. However, you can define a predicate cond, and use it in the assumes clauses of the behaviors and everywhere else. > > BTW, I believe the ACSL manual, sections 2.3.3, 2.3.4 is wrong on the > equivalence of named and regular contract as stated on p. 30. You're right. The global requires clause makes regular contract quite specific. Best regards, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98