class Rational
{
  var n : int
  var m : int // nu permit m == 0

  ghost predicate valid()
    reads this
  {
    m != 0
  }

  ghost function value() : real
    reads this
    requires this.valid()
  {
    (n as real) / (m as real)
  }
  
  constructor(n' : int, m' : int)
    requires m' != 0
    ensures valid()
    ensures n == n'
    ensures m == m'
  {
    n := n';
    m := m';
  }

  constructor fromInt(x : int)
    ensures valid()
    ensures value() == x as real
  {
    n := x;
    m := 1;
  }

  method add(o : Rational) returns (r : Rational)
    requires this.valid()
    requires o.valid()
    ensures r.valid()
    ensures r.value() == this.value() + o.value()
  {
    // n / m + o.n / o.m = n * o.m / m * o.m + o.n * m / o.m * m
    var newn : int := n * o.m +  o.n * m;
    var newm : int := m * o.m;
    r := new Rational(newn, newm);
    calc {
      value() + o.value();
      ==
        (n as real) / (m as real) + (o.n as real) / (o.m as real);
        ==
          (((n as real) * (o.m as real)) / ((m as real) * (o.m as real))) +
          ((o.n as real) * (m as real)) / ((o.m as real) * (m as real));
          ==
            ((n * o.m) as real) / ((m * o.m) as real) +
            ((o.n * m) as real) / ((o.m * m) as real);
            ==
              (((n * o.m) as real) + ((o.n * m) as real)) / ((m * o.m) as real);
              ==
                (((n * o.m) + (o.n * m)) as real) / ((m * o.m) as real);
              ==
                newn as real / newm as real;
                ==
                  r.value();
    }
  }
  
  method add'(o : Rational)
    //requires this != o
    requires this.valid()
    requires o.valid()
    ensures this.valid()
    modifies this
    ensures this.value() == old(this.value()) + old(o.value())
  {
    // n / m + o.n / o.m = n * o.m / m * o.m + o.n * m / o.m * m
    calc {
      old(value()) + o.value();
      ==
        (n as real) / (m as real) + (o.n as real) / (o.m as real);
        ==
          (((n as real) * (o.m as real)) / ((m as real) * (o.m as real))) +
          ((o.n as real) * (m as real)) / ((o.m as real) * (m as real));
          ==
            ((n * o.m) as real) / ((m * o.m) as real) +
            ((o.n * m) as real) / ((o.m * m) as real);
            ==
              (((n * o.m) as real) + ((o.n * m) as real)) / ((m * o.m) as real);
              ==
                (((n * o.m) + (o.n * m)) as real) / ((m * o.m) as real);
    }
    assert old(value()) + o.value() == (((n * o.m) + (o.n * m)) as real) / ((m * o.m) as real);
    n := n * o.m + o.n * m;
    m := m * o.m;
    assert value() == (n as real) / (m  as real);
  }
}