JML

org.jmlspecs.samples.dbc
Class Rectangular

java.lang.Object
  extended byorg.jmlspecs.samples.dbc.ComplexOps
      extended byorg.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.

Constructor Detail

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());
Method Detail

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;

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.