Mean.scala [raw]


/* Copyright 2009-2016 EPFL, Lausanne */

import stainless.annotation._
import stainless.lang._

object Mean {

  def meanOverflow(x: Int, y: Int): Int = {
    require(x <= y && x >= 0 && y >= 0)
    (x + y)/2
  } ensuring(m => m >= x && m <= y)
// Counterexample for postcondition violation in `meanOverflow`:
//   when y is:
//     1865154560
//   when x is:
//     1277440000

}

back