org.jmlspecs.samples.dbc
Class Polar

java.lang.Object
  org.jmlspecs.samples.dbc.ComplexOps
      org.jmlspecs.samples.dbc.Polar

All Implemented Interfaces:

Complex

public strictfp class Polar

extends ComplexOps

Complex numbers in polar coordinates.

Author:

Gary T. Leavens with help from Abelson and Sussman's Structure and Interpretation of Computer Programs

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Complex

axiom ( \forall double d, dd; dd > 0.0; d%dd > -dd&&d%dd < dd); axiom ( \forall double d, dd; ; d > -dd ==> d+dd > 0.0);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Ghost fields inherited from interface org.jmlspecs.samples.dbc.Complex

tolerance

 

Field Summary
private  double	ang           The angle of this number.
private  double	mag           The magnitude of this number.

 

Constructor Summary

Polar(double mag, double ang)           Initialize this polar coordinate number with magnitude mag and angle ang, except that when the magnitude is negative, this is interpreted as magnitude -mag and angle ang+StrictMath.PI.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface org.jmlspecs.samples.dbc.Complex

positiveRemainder, similarAngle

 

Method Summary
double	angle()           Return the angle of this complex number.
double	imaginaryPart()           Return the imaginary part of this complex number.
double	magnitude()           Return the magnitude of this complex number.
double	realPart()           Return the real part of this complex number.
static double	standardizeAngle(double rad)           Standardize the angle so it's between -StrictMath.PI and StrictMath.PI (radians).
String	toString()

 

Methods inherited from class org.jmlspecs.samples.dbc.ComplexOps

add, div, equals, hashCode, mul, sub

 

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

mag

private double mag

The magnitude of this number.

ang

private double ang

The angle of this number.

Polar

public Polar(double mag,
             double ang)
      throws IllegalArgumentException

Initialize this polar coordinate number with magnitude mag and angle ang, except that when the magnitude is negative, this is interpreted as magnitude -mag and angle ang+StrictMath.PI.

Parameters:

mag - the magnitude desired

ang - the angle in radians, measured counterclockwise from the positive x axis

Throws:

IllegalArgumentException

Specifications: (class)pure

requires mag >= 0.0&&-Infinity < ang&&ang < Infinity;
ensures this.magnitude() == mag;
ensures this.angle() == standardizeAngle(ang);

     also

requires mag < 0.0&&-Infinity < ang&&ang < Infinity;
ensures this.magnitude() == -mag;
ensures this.angle() == standardizeAngle(ang+3.141592653589793);

     also

requires java.lang.Double.isNaN(mag)||java.lang.Double.isNaN(ang)||-Infinity == ang||ang == Infinity;
signals_only java.lang.IllegalArgumentException;

standardizeAngle

public static double standardizeAngle(double rad)
                               throws IllegalArgumentException

Standardize the angle so it's between -StrictMath.PI and StrictMath.PI (radians).

Throws:

IllegalArgumentException

Specifications: pure

requires -Infinity < rad&&rad < Infinity;
ensures -3.141592653589793 <= \result &&\result <= 3.141592653589793;

     also

requires java.lang.Double.isNaN(rad)||-Infinity == rad||rad == Infinity;
signals_only java.lang.IllegalArgumentException;

realPart

public double realPart()

Description copied from interface: Complex

Return the real part of this complex number.

Specifications: (class)pure

Specifications inherited from overridden method in interface Complex:
       (class)pure

ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.magnitude()*java.lang.StrictMath.cos(this.angle()),\result ,0.0050);

imaginaryPart

public double imaginaryPart()

Description copied from interface: Complex

Return the imaginary part of this complex number.

Specifications: (class)pure

Specifications inherited from overridden method in interface Complex:
       (class)pure

ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(\result ,this.magnitude()*java.lang.StrictMath.sin(this.angle()),0.0050);

magnitude

public double magnitude()

Description copied from interface: Complex

Return the magnitude of this complex number.

Specifications: (class)pure

Specifications inherited from overridden method in interface Complex:
       (class)pure

ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(java.lang.StrictMath.sqrt(this.realPart()*this.realPart()+this.imaginaryPart()*this.imaginaryPart()),\result ,0.0050);

angle

public double angle()

Description copied from interface: Complex

Return the angle of this complex number.

Specifications: (class)pure

Specifications inherited from overridden method in interface Complex:
       (class)pure

ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(java.lang.StrictMath.atan2(this.imaginaryPart(),this.realPart()),\result ,0.0050);

toString

public String toString()

Overrides:

toString in class Object

Specifications: (class)pure

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;