Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Specifying function monotonicity in ACSL
  • From: lc at adelard.com (Lukasz Cyra)
  • Date: Tue, 21 Jul 2009 10:51:29 +0100
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