package cs362practice;

//@ model import org.jmlspecs.models.JMLDouble;

/** Complex numbers.  Note that these are immutable.
 * Abstractly, one can think of a complex number as
 *  realPart+(imaginaryPart*i).
 * Alternatively, one can think of it as distance
 * from the origin along a given angle 
 * (measured in radians counterclockwise from
 * the positive x axis), hence a pair of
 *  (magnitude, angle).
 * This class supports both of these views.
 */
public /*@ pure @*/ interface Complex {
    
    //@ public ghost static final double tolerance = 0.005;
    
    /** Return the real part of this complex number. */
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             magnitude()*Math.cos(angle()),
      @             \result,
      @             tolerance);
      @*/  
    double realPart();
    
    /** Return the imaginary part of this complex number. */
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             \result,
      @             magnitude()*Math.sin(angle()),
      @             tolerance);
      @*/  
    double imaginaryPart();

    /** Return the magnitude of this complex number. */
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             Math.sqrt(realPart()*realPart()
      @                       + imaginaryPart()*imaginaryPart()),
      @             \result,
      @             tolerance);
      @*/
    double magnitude();
    
    /** Return the angle of this complex number. */
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             Math.atan2(imaginaryPart(), realPart()),
      @             \result,
      @             tolerance);
      @*/
    double angle();
    
    /** Return this + b (the sum of this and b). */
    //@ requires b != null; 
    //@ ensures \result != null;
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             this.realPart() + b.realPart(),
      @             \result.realPart(),
      @             tolerance);
      @ ensures JMLDouble.approximatelyEqualTo(
      @             this.imaginaryPart() + b.imaginaryPart(),
      @             \result.imaginaryPart(),
      @             tolerance);
      @*/
    Complex add(Complex b);
    
    /** Return this - b (the difference between this and b). */
    //@ requires b != null; 
    //@ ensures \result != null;
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             this.realPart() - b.realPart(),
      @             \result.realPart(),
      @             tolerance);
      @ ensures JMLDouble.approximatelyEqualTo(
      @             this.imaginaryPart() - b.imaginaryPart(),
      @             \result.imaginaryPart(),
      @             tolerance);
      @*/
    Complex sub(Complex b);
    
    /** Tell whether the given angles are the same, taking into account
     *  that angles measured in radians wrap around after 2*Math.PI times.
     */
    /*@ public model pure boolean similarAngle(double ang1, double ang2) {
      @    ang1 = positiveRemainder(ang1, 2*Math.PI);
      @    ang2 = positiveRemainder(ang2, 2*Math.PI);
      @    return JMLDouble.approximatelyEqualTo(ang1, ang2, tolerance);
      @ }
      @*/
    
    /** Return the positive remainder of n divided by d. */
    /*@ ensures \result >= 0.0;
      @ public model pure double positiveRemainder(double n, double d) {
      @    n = n % d;
      @    if (n < 0) {
      @       n += d;
      @    }
      @    return d;
      @ }
      @*/

    /** Return this * b (the product of this and b). */
    //@ requires b != null; 
    //@ ensures \result != null;
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             this.magnitude() * b.magnitude(),
      @             \result.magnitude(),
      @             tolerance);
      @ ensures similarAngle(this.angle() + b.angle(),
      @                      \result.angle());
      @*/
    Complex mul(Complex b);
    
    /** Return this/b (the quotient of this by b). */
    //@ requires b != null && b.magnitude() != 0; 
    //@ ensures \result != null;
    /*@ ensures JMLDouble.approximatelyEqualTo(
      @             this.magnitude() / b.magnitude(),
      @             \result.magnitude(),
      @             tolerance);
      @ ensures similarAngle(this.angle() - b.angle(),
      @                      \result.angle());
      @*/
    Complex div(Complex b);
    
    /** Return true if these are the same complex number. */
    /*@ also
      @ ensures \result
      @     <==> o instanceof Complex
      @          && this.realPart() == ((Complex)o).realPart()
      @          && this.imaginaryPart() == ((Complex)o).imaginaryPart();
      @ ensures \result 
      @     <==> o instanceof Complex
      @          && this.magnitude() == ((Complex)o).magnitude()
      @          && this.angle() == ((Complex)o).angle();
      @*/
    boolean equals(Object o);

    /** Return a hashCode for this number. */
    // specification inherited
    int hashCode();
}