frama-cexample

min.c

typedef enum _bool { false = 0, true = 1 } bool ;

typedef void* T;

/*@
axiomatic Order{
  predicate LE(T x, T y);
  axiom refl: \forall T x; LE(x,x);
  axiom trans: \forall T x, T y, T z; LE(x,y) && LE(y,z) ==> LE(x,z);
}
*/

/*@
  ensures (\result == true ==> LE(x,y)) && (\result == false  ==> LE(y, x));
 */
bool le_(T x, T y) { return true; }

/*@
  ensures LE(\result,x) && LE(\result, y);
 */
T min(T x, T y){
  return le_(x,y) ? x : y;
}

/*@
  ensures LE(\result,x) && LE(\result, y) && LE(\result, z);
 */
T min3(T x, T y, T z){
  return min(x, min(y,z));
}