JML

## 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`
 Model Method Detail

### 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;
 Method Detail

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

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

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.