--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on January 2014 ---
Hello, 2014/1/27 Dharmalingam Ganesan <dganesan at fc-md.umd.edu>: > For this example, some of my behaviors share a set of assumes. For example, HighSaO2, LowSaO2, and RoundSaO2 share the assumes !Is_Adv_or_Mon_Failed predicate. > > Is there a possibility to declare assumes that are shared by a set of behaviors only once, just to make the behavioral spec lean? > Not quite: there is no notion of "sub-behavior" in ACSL. The closest you can have is, as you did, to define a predicate for the common part. A somehow contrived specification could use statement contracts for the whole body of the function and the 'for foo:' clause, but statement contracts cannot use the \result keyword in their ensures clause, and the returns clause is not well supported by WP (this is also the case for 'for foo:'), so that this approach will not work very well in practice. Here is nevertheless an example: /*@ behavior foo: assumes a == 0; */ int foo(int a, int b) { /*@ for foo: behavior foo_1: assumes b == 0; returns \result == 0; behavior foo_2: assumes b > 0; returns \result == 1; behavior foo_3: assumes b < 0; returns \result == -1; complete behaviors; disjoint behaviors; */ { if (a==0) { if (b == 0) return 0; if (b<0) return -1; else return 1; } return 2; } } Best regards, -- E tutto per oggi, a la prossima volta Virgile