--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2009 ---
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