org.jmlspecs.samples.dbc
Interface Complex

All Known Implementing Classes:

ComplexOps

public interface Complex

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. The specifications in this class are intentionally of the lightweight variety.

Author:

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

Class Specifications

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);

Specifications inherited from class Object

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

Ghost Field Summary
static double	tolerance

 

Model Method Summary
double	positiveRemainder(double n, double d)           Return the positive remainder of n divided by d.
boolean	similarAngle(double ang1, double ang2)           Tell whether the given angles are the same, taking into account that angles measured in radians wrap around after 2*StrictMath.PI times.

 

Method Summary
Complex	add(Complex b)           Return this + b (the sum of this and b).
double	angle()           Return the angle of this complex number.
Complex	div(Complex b)           Return this/b (the quotient of this by b).
boolean	equals(nullable Object o)           Return true if these are the same complex number.
int	hashCode()           Return a hashCode for this number.
double	imaginaryPart()           Return the imaginary part of this complex number.
double	magnitude()           Return the magnitude of this complex number.
Complex	mul(Complex b)           Return this * b (the product of this and b).
double	realPart()           Return the real part of this complex number.
Complex	sub(Complex b)           Return this - b (the difference between this and b).

 

Ghost Field Detail

tolerance

public static final double tolerance

similarAngle

public boolean similarAngle(double ang1,
                            double ang2)

Tell whether the given angles are the same, taking into account that angles measured in radians wrap around after 2*StrictMath.PI times.

Specifications: pure

positiveRemainder

public double positiveRemainder(double n,
                                double d)

Return the positive remainder of n divided by d.

Specifications: pure

requires d > 0.0;
ensures \result >= 0.0;

realPart

public double realPart()

Return the real part of this complex number.

Specifications: (class)pure

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

imaginaryPart

public double imaginaryPart()

Return the imaginary part of this complex number.

Specifications: (class)pure

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

magnitude

public double magnitude()

Return the magnitude of this complex number.

Specifications: (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()

Return the angle of this complex number.

Specifications: (class)pure

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

add

public Complex add(Complex b)

Return this + b (the sum of this and b).

Specifications: (class)pure

requires_redundantly b != null;
ensures_redundantly \result != null;
ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.realPart()+b.realPart(),\result .realPart(),0.0050);
ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.imaginaryPart()+b.imaginaryPart(),\result .imaginaryPart(),0.0050);

sub

public Complex sub(Complex b)

Return this - b (the difference between this and b).

Specifications: (class)pure

requires_redundantly b != null;
ensures_redundantly \result != null;
ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.realPart()-b.realPart(),\result .realPart(),0.0050);
ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.imaginaryPart()-b.imaginaryPart(),\result .imaginaryPart(),0.0050);

mul

public Complex mul(Complex b)

Return this * b (the product of this and b).

Specifications: (class)pure

requires_redundantly b != null;
requires !java.lang.Double.isNaN(this.magnitude()*b.magnitude());
requires !java.lang.Double.isNaN(this.angle())&&!java.lang.Double.isNaN(b.angle());
ensures_redundantly \result != null;
ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.magnitude()*b.magnitude(),\result .magnitude(),0.0050);
ensures this.similarAngle(this.angle()+b.angle(),\result .angle());

     also

requires_redundantly b != null;
requires java.lang.Double.isNaN(this.magnitude()*b.magnitude())||java.lang.Double.isNaN(this.angle())||java.lang.Double.isNaN(b.angle());
ensures java.lang.Double.isNaN(\result .realPart());
ensures \result .imaginaryPart() == 0.0;

div

public Complex div(Complex b)

Return this/b (the quotient of this by b).

Specifications: (class)pure

requires_redundantly b != null;
requires !java.lang.Double.isNaN(this.magnitude()/b.magnitude());
requires !java.lang.Double.isNaN(this.angle())&&!java.lang.Double.isNaN(b.angle());
ensures_redundantly \result != null;
ensures org.jmlspecs.models.JMLDouble.approximatelyEqualTo(this.magnitude()/b.magnitude(),\result .magnitude(),0.0050);
ensures this.similarAngle(this.angle()-b.angle(),\result .angle());

     also

requires_redundantly b != null;
requires java.lang.Double.isNaN(this.magnitude()/b.magnitude())||java.lang.Double.isNaN(this.angle())||java.lang.Double.isNaN(b.angle());
ensures java.lang.Double.isNaN(\result .realPart());
ensures \result .imaginaryPart() == 0.0;

equals

public boolean equals(nullable Object o)

Return true if these are the same complex number.

Overrides:

equals in class Object

Specifications: (class)pure

     also

ensures \result <==> o instanceof org.jmlspecs.samples.dbc.Complex&&this.realPart() == ((org.jmlspecs.samples.dbc.Complex)o).realPart()&&this.imaginaryPart() == ((org.jmlspecs.samples.dbc.Complex)o).imaginaryPart();
ensures \result <==> o instanceof org.jmlspecs.samples.dbc.Complex&&this.magnitude() == ((org.jmlspecs.samples.dbc.Complex)o).magnitude()&&this.angle() == ((org.jmlspecs.samples.dbc.Complex)o).angle();

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

hashCode

public int hashCode()

Return a hashCode for this number.

Overrides:

hashCode in class Object

Specifications: (class)pure

Specifications inherited from overridden method in class Object:

public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);

     also

public code normal_behavior
assignable \nothing;