object FirstStepsWithStainless {
    def commutativity(x: Long, y: Long): Unit = {
    } ensuring(res => x + y == y + x)

    def f(x: BigInt,y: BigInt): BigInt = {
      require(x >= 0 && y >= 0)
      x + y 
    } ensuring(res => res >= 0)

    def fVC(x: BigInt, y:BigInt): Unit = {
    } ensuring(_ => (!(x >= 0 && y >= 0) || x + y >= 0))    

    def assoc(x: BigInt, y:BigInt, z:BigInt): Unit ={
      require(x >= 0 && y >= 0 && z >= 0)
    } ensuring(_ => f(f(x,y),z) == f(x, f(y,z)))

    // multiplication of fractions: (p1/q1) * (p2/q2)
    def mul(p1: BigInt, q1: BigInt,  // p1/q1
            p2: BigInt, q2: BigInt): (BigInt, BigInt) = 
    {
      require(q1 > 0 && q2 > 0)
      val (p,q) = (p1*p2, q1*q2)
      (p,q)
    } ensuring (res => res._2 > 0)

    // division of fractions: (p1/q1) / (p2/q2)
    def div(p1: BigInt, q1: BigInt,
            p2: BigInt, q2: BigInt): (BigInt, BigInt) = 
    {
      require(q1 > 0 && q2 > 0)
      val (p,q) = (p1*q2, q1*p2)
      if (q > 0) (p,q)
      else (-p, -q)
    } ensuring (res => res._2 > 0)
}
