Ryan

class Fraction:
    __metaclass__ = dbc.DbcMeta

    @dbc.contract
    def __init__(self, numerator, denominator=1):
        self.numerator = numerator
        self.denominator = denominator
        self._cancel_down()

    @__init__.ensure
    def __init__(returned, self, numerator, denominator=1):
        assert (self.numerator / self.denominator) == (numerator / denominator), \
            "%s != %s" % (self.numerator/self.denominator, numerator/denominator)


    def __str__(self):
        return str(self.numerator) + '/' + str(self.denominator)

    def __repr__(self):
        return str(self)

    def __eq__(self, other):
        return (self.numerator/self.denominator) == other

    @dbc.contract
    def reciprocal(self):
        return Fraction(self.denominator, self.numerator)

    @reciprocal.require
    def reciprocal(self):
        assert self.numerator != 0, "Numerator cannot be 0"

    @reciprocal.ensure
    def reciprocal(returned, self):
        assert returned * self == 1, "self * returned != 1"

    @dbc.contract
    def __neg__(self):
        return Fraction(-self.numerator, self.denominator)

    @__neg__.ensure
    def __neg__(returned, self):
        assert returned.numerator == -self.numerator
        assert returned.denominator == self.denominator

    def __pos__(self):
        return self

    def __add__(self, other):
        return Fraction(self.numerator*other.denominator +
                        other.numerator*self.denominator,
                        self.denominator*self.denominator)

    def __sub__(self, other):
        return self + (-other)

    def __mul__(self, other):
        return Fraction(self.numerator*other.numerator,
                        self.denominator*other.denominator)

    def __div__(self, other):
        return self * other.reciprocal()

    def _cancel_down(self):
        sign = 1
        if self.denominator < 0:
            sign = -sign
            self.denominator = abs(self.denominator)
        if self.numerator < 0:
            sign = -sign
            self.numerator = abs(self.numerator)

        divisor = self.gcd(self.numerator, self.denominator)
        self.numerator = sign * (self.numerator // divisor)
        self.denominator = self.denominator // divisor

    @dbc.contract
    def gcd(self, x, y):
        v = y
        result = x
        while v != 0:
            remainder = result % v
            result = v
            v = remainder
        return result or 1

    @gcd.require
    def gcd(self, x, y):
        assert x >= 0, "x should be nonnegative"
        assert y >= 0, "y should be nonnegative"

    @gcd.ensure
    def gcd(returned, self, x,y):
        assert returned == self.gcd.method(self, y,x)

    def invariant(self):
        assert self.denominator != 0
        assert self == self
        assert self - self == 0