Skip to content
Snippets Groups Projects
Commit 96449c61 authored by Regis Blanc's avatar Regis Blanc
Browse files

no need for isRat postconditions

parent ad6b90b5
Branches
Tags
No related merge requests found
...@@ -13,31 +13,31 @@ case class Rational(numerator: BigInt, denominator: BigInt) { ...@@ -13,31 +13,31 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
def +(that: Rational): Rational = { def +(that: Rational): Rational = {
Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator) Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
} ensuring(res => res.isRational) }
def -(that: Rational): Rational = { def -(that: Rational): Rational = {
Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator) Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
} ensuring(res => res.isRational) }
def unary_- : Rational = { def unary_- : Rational = {
Rational(-this.numerator, this.denominator) Rational(-this.numerator, this.denominator)
} ensuring(res => res.isRational) }
def *(that: Rational): Rational = { def *(that: Rational): Rational = {
Rational(this.numerator*that.numerator, this.denominator*that.denominator) Rational(this.numerator*that.numerator, this.denominator*that.denominator)
} ensuring(res => res.isRational) }
def /(that: Rational): Rational = { def /(that: Rational): Rational = {
require(that.nonZero) require(that.nonZero)
val newNumerator = this.numerator*that.denominator val newNumerator = this.numerator*that.denominator
val newDenominator = this.denominator*that.numerator val newDenominator = this.denominator*that.numerator
normalize(newNumerator, newDenominator) normalize(newNumerator, newDenominator)
} ensuring(res => res.isRational) }
def reciprocal: Rational = { def reciprocal: Rational = {
require(this.nonZero) require(this.nonZero)
normalize(this.denominator, this.numerator) normalize(this.denominator, this.numerator)
} ensuring(res => res.isRational) }
def ~(that: Rational): Boolean = { def ~(that: Rational): Boolean = {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment