--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP - How to represent duplicate assumes?



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