org.jmlspecs.samples.dbc
Class Rectangular

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

All Implemented Interfaces:

Complex

public strictfp class Rectangular

extends ComplexOps

Complex numbers in rectangular 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	img           The imaginary part of this number.
private  double	re           The real part of this number.

 

Constructor Summary

Rectangular()           Initialize this Complex number to be 0+(0*i).

Rectangular(double re)           Initialize this Complex number to be re+(0*i).

Rectangular(double re, double img)           Initialize this Complex number to be re+(img*i).

 

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.
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

re

private double re

The real part of this number.

img

private double img

The imaginary part of this number.

Rectangular

public Rectangular()

Initialize this Complex number to be 0+(0*i).

Specifications: (class)pure

ensures this.realPart() == 0.0&&this.imaginaryPart() == 0.0;

Rectangular

public Rectangular(double re)

Initialize this Complex number to be re+(0*i).

Specifications: (class)pure

requires !java.lang.Double.isNaN(re);
ensures this.realPart() == re&&this.imaginaryPart() == 0.0;

     also

requires java.lang.Double.isNaN(re);
ensures java.lang.Double.isNaN(this.realPart())&&this.imaginaryPart() == 0.0;

Rectangular

public Rectangular(double re,
                   double img)

Initialize this Complex number to be re+(img*i).

Specifications: (class)pure

ensures !java.lang.Double.isNaN(re) ==> this.realPart() == re;
ensures !java.lang.Double.isNaN(img) ==> this.imaginaryPart() == img;
ensures java.lang.Double.isNaN(re) ==> java.lang.Double.isNaN(this.realPart());
ensures java.lang.Double.isNaN(img) ==> java.lang.Double.isNaN(this.imaginaryPart());

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;