--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Specifying function monotonicity in ACSL



Hello,



I am trying to specify that a function is increasing monotonic. Is it possible to do it in ACSL only, without adding extra c code?

What I have done at the moment is adding to the code an extra function as presented below.

The problem with such a solution is that I cannot prove monotonicity of more sophisticated functions this way, e.g. lets say that I have two functions f() and g(). I demonstrated that g() is monotonic. My approach does not help me in demonstrating that supersposition of these functions f(g(x)) is monotonic. If monotonicity was expressed using ACSL only I would probobly be able to demonstrate it easily.



// the function of interest

int f(int x) {

// body of f()

}

/*@ behavior monotonicity:

  @ ensures x > y ==> \result == 1;

  @*/

int extra_code(int x, int y) {

   return f(x) >= f(y) ? 1 : 0;

}

Best regards
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090721/2c573565/attachment.htm