rational invariant positive denominator

library/lang/Rational.scala

@@ -12,32 +12,34 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
   def +(that: Rational): Rational = {
     require(this.isRational && that.isRational)
     Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
-  }
+  } ensuring(res => res.isRational)
 
   def -(that: Rational): Rational = {
     require(this.isRational && that.isRational)
     Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
-  }
+  } ensuring(res => res.isRational)
 
   def unary_- : Rational = {
     require(this.isRational)
     Rational(-this.numerator, this.denominator)
-  }
+  } ensuring(res => res.isRational)
 
   def *(that: Rational): Rational = {
     require(this.isRational && that.isRational)
     Rational(this.numerator*that.numerator, this.denominator*that.denominator)
-  }
+  } ensuring(res => res.isRational)
 
   def /(that: Rational): Rational = {
     require(this.isRational && that.isRational && that.nonZero)
-    Rational(this.numerator*that.denominator, this.denominator*that.numerator)
-  }
+    val newNumerator = this.numerator*that.denominator
+    val newDenominator = this.denominator*that.numerator
+    normalize(newNumerator, newDenominator)
+  } ensuring(res => res.isRational)
 
   def reciprocal: Rational = {
     require(this.isRational && this.nonZero)
-    Rational(this.denominator, this.numerator)
-  }
+    normalize(this.denominator, this.numerator)
+  } ensuring(res => res.isRational)
 
 
   def ~(that: Rational): Boolean = {
@@ -47,50 +49,22 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
 
   def <(that: Rational): Boolean = {
     require(this.isRational && that.isRational)
-    if(this.denominator >= 0 && that.denominator >= 0)
-      this.numerator*that.denominator < that.numerator*this.denominator
-    else if(this.denominator >= 0 && that.denominator < 0)
-      this.numerator*that.denominator > that.numerator*this.denominator
-    else if(this.denominator < 0 && that.denominator >= 0)
-      this.numerator*that.denominator > that.numerator*this.denominator
-    else
-      this.numerator*that.denominator < that.numerator*this.denominator
+    this.numerator*that.denominator < that.numerator*this.denominator
   }
 
   def <=(that: Rational): Boolean = {
     require(this.isRational && that.isRational)
-    if(this.denominator >= 0 && that.denominator >= 0)
-      this.numerator*that.denominator <= that.numerator*this.denominator
-    else if(this.denominator >= 0 && that.denominator < 0)
-      this.numerator*that.denominator >= that.numerator*this.denominator
-    else if(this.denominator < 0 && that.denominator >= 0)
-      this.numerator*that.denominator >= that.numerator*this.denominator
-    else
-      this.numerator*that.denominator <= that.numerator*this.denominator
+    this.numerator*that.denominator <= that.numerator*this.denominator
   }
 
   def >(that: Rational): Boolean = {
     require(this.isRational && that.isRational)
-    if(this.denominator >= 0 && that.denominator >= 0)
-      this.numerator*that.denominator > that.numerator*this.denominator
-    else if(this.denominator >= 0 && that.denominator < 0)
-      this.numerator*that.denominator < that.numerator*this.denominator
-    else if(this.denominator < 0 && that.denominator >= 0)
-      this.numerator*that.denominator < that.numerator*this.denominator
-    else
-      this.numerator*that.denominator > that.numerator*this.denominator
+    this.numerator*that.denominator > that.numerator*this.denominator
   }
 
   def >=(that: Rational): Boolean = {
     require(this.isRational && that.isRational)
-    if(this.denominator >= 0 && that.denominator >= 0)
-      this.numerator*that.denominator >= that.numerator*this.denominator
-    else if(this.denominator >= 0 && that.denominator < 0)
-      this.numerator*that.denominator <= that.numerator*this.denominator
-    else if(this.denominator < 0 && that.denominator >= 0)
-      this.numerator*that.denominator <= that.numerator*this.denominator
-    else
-      this.numerator*that.denominator >= that.numerator*this.denominator
+    this.numerator*that.denominator >= that.numerator*this.denominator
   }
 
   def nonZero: Boolean = {
@@ -98,7 +72,14 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
     numerator != 0
   }
 
-  def isRational: Boolean = denominator != 0
+  def isRational: Boolean = denominator > 0
+
+  private def normalize(num: BigInt, den: BigInt): Rational = {
+    if(den < 0)
+      Rational(-num, -den)
+    else
+      Rational(num, den)
+  }
 }
 
 object Rational {

testcases/verification/math/RationalProps.scala

@@ -2,6 +2,8 @@ import leon.lang._
 import leon.collection._
 import leon._
 
+import scala.language.postfixOps
+
 object RationalProps {
 
   def squarePos(r: Rational): Rational = {