JML

org.jmlspecs.models
Interface JMLInfiniteInteger

All Superinterfaces:
Cloneable, Comparable, JMLComparable, JMLType, Serializable
All Known Implementing Classes:
JMLInfiniteIntegerClass

public interface JMLInfiniteInteger
extends JMLComparable

Infinite precision integers with an plus and minus infinity.

This type is intended to support reasoning like that done by Eric Hehner for the time behavior of programs. Of course, it could also be used for other purposes as well.

Version:
$Revision: 1.35 $
Author:
Gary T. Leavens
See Also:
BigInteger

Class Specifications
public invariant this.sign == -1||this.sign == 0||this.sign == 1;
instance public invariant this.sign == -1||this.sign == 0||this.sign == 1;
instance public invariant !this.is_infinite ==> this.finite_value != null&&this.sign == this.finite_value.signum();
instance public invariant_redundantly this.sign == 0 <==> !this.is_infinite&&this.finite_value.equals(java.math.BigInteger.ZERO);
instance public constraint this.nonnegative == \old(this.nonnegative);
instance public constraint this.sign == \old(this.sign);
instance public constraint this.is_infinite == \old(this.is_infinite);
instance public constraint this.finite_value == \old(this.finite_value);
instance public represents nonnegative <- this.sign >= 0;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface Comparable
instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0);
instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x)));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Model Field Summary
[instance]  BigInteger finite_value
          If this integer is not infinite, its finite value.
[instance]  boolean is_infinite
          Is this integer infinite?
[instance]  boolean nonnegative
          Does this object represent a nonnegative integer?
[instance]  int sign
          The sign of this integer.
 
Model Method Summary
 
Model methods inherited from interface java.lang.Comparable
definedComparison, sgn
 
Method Summary
 JMLInfiniteInteger abs()
          Return the absolute value of this integer.
 JMLInfiniteInteger add(non_null JMLInfiniteInteger n)
          Return the sum of this integer and the argument.
 int compareTo(non_null Object o)
          Compare this to o, returning a comparison code.
 JMLInfiniteInteger divide(non_null JMLInfiniteInteger n)
          Return the quotient of this integer divided by the argument.
 double doubleValue()
          Return this integer approximated by a double.
 boolean equals(nullable Object o)
          Tell whether this integer is equal to the argument.
 BigInteger finiteValue()
          Assuming this integer is finite, return its value.
 float floatValue()
          Return this integer approximated by a float.
 boolean greaterThan(non_null JMLInfiniteInteger n)
          Tell if this integer is strictly greater than the argument.
 boolean greaterThanOrEqualTo(non_null JMLInfiniteInteger n)
          Tell if this integer is greater than or equal to the argument.
 int hashCode()
          Return a hash code for this integer.
 boolean isFinite()
          Tell if this integer is finite.
 boolean lessThan(non_null JMLInfiniteInteger n)
          Tell if this integer is strictly less than the argument.
 boolean lessThanOrEqualTo(non_null JMLInfiniteInteger n)
          Tell if this integer is less than or equal to the argument.
 JMLInfiniteInteger max(non_null JMLInfiniteInteger n)
          Return the maximum of this integer and the argument.
 JMLInfiniteInteger min(non_null JMLInfiniteInteger n)
          Return the minimum of this integer and the argument.
 JMLInfiniteInteger mod(non_null JMLInfiniteInteger n)
          Return this integer modulo the argument.
 JMLInfiniteInteger multiply(non_null JMLInfiniteInteger n)
          Return the product of this integer and the argument.
 JMLInfiniteInteger negate()
          Return the negation of this integer.
 JMLInfiniteInteger pow(int n)
          Return this integer raised to the argument's power.
 JMLInfiniteInteger remainder(non_null JMLInfiniteInteger n)
          Return the remainder of this integer divided by the argument.
 int signum()
          Return the sign of this integer.
 JMLInfiniteInteger subtract(non_null JMLInfiniteInteger n)
          Return the difference between this integer and the argument.
 String toString()
          Return the decimal representation of this integer.
 String toString(int radix)
          Return the digits representing this integer in the given radix.
 
Methods inherited from interface org.jmlspecs.models.JMLType
clone
 

Model Field Detail

nonnegative

public boolean nonnegative
Does this object represent a nonnegative integer?

Specifications: instance
datagroup contains: sign

sign

public int sign
The sign of this integer.

Specifications: instance
is in groups: nonnegative
datagroup contains: org.jmlspecs.models.JMLFiniteInteger.val

is_infinite

public boolean is_infinite
Is this integer infinite?

Specifications: instance
datagroup contains: org.jmlspecs.models.JMLFiniteInteger.val

finite_value

public BigInteger finite_value
If this integer is not infinite, its finite value.

Specifications: instance
datagroup contains: org.jmlspecs.models.JMLFiniteInteger.val
Method Detail

signum

public int signum()
Return the sign of this integer.

Specifications: (class)pure
public normal_behavior
ensures \result == this.sign;
    implies_that
public normal_behavior
ensures \result == -1||\result == 0||\result == 1;
ensures (\result == 0||\result == 1) <==> this.nonnegative;
ensures \result == -1 <==> !this.nonnegative;

isFinite

public boolean isFinite()
Tell if this integer is finite.

Specifications: (class)pure
public normal_behavior
ensures \result == !this.is_infinite;

finiteValue

public BigInteger finiteValue()
                                throws ArithmeticException
Assuming this integer is finite, return its value.

Throws:
ArithmeticException
Specifications: non_null (class)pure
public normal_behavior
requires !this.is_infinite;
ensures \result != null&&\result .equals(this.finite_value);
     also
public exceptional_behavior
requires this.is_infinite;
signals_only java.lang.ArithmeticException;

compareTo

public int compareTo(non_null Object o)
                       throws ClassCastException
Compare this to o, returning a comparison code.

Specified by:
compareTo in interface JMLComparable
Parameters:
o - the object this is compared to.
Throws:
ClassCastException - when o is not a JMLInfiniteInteger or a BigInteger.
See Also:
equals(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: (class)pure
     also
public normal_behavior
requires o != null&&o instanceof org.jmlspecs.models.JMLInfiniteInteger;
{|
old org.jmlspecs.models.JMLInfiniteInteger n = (org.jmlspecs.models.JMLInfiniteInteger)o;
{|
requires this.lessThan(n);
ensures \result == -1;
also
requires this.equals(n);
ensures \result == 0;
also
requires this.greaterThan(n);
ensures \result == 1;
|}
|}
     also
public normal_behavior
requires o != null&&o instanceof java.math.BigInteger;
{|
requires this.is_infinite&&!this.nonnegative;
ensures \result == -1;
also
requires !this.is_infinite;
ensures \result == this.finite_value.compareTo((java.math.BigInteger)o);
also
requires this.is_infinite&&this.nonnegative;
ensures \result == 1;
|}
     also
public exceptional_behavior
requires o != null&&!(o instanceof org.jmlspecs.models.JMLInfiniteInteger)&&!(o instanceof java.math.BigInteger);
signals_only java.lang.ClassCastException;
Specifications inherited from overridden method compareTo(Object o) in interface JMLComparable:
       (class)pure
     also
public behavior
requires o != null;
ensures (* o is an instance of a comparable class *);
ensures (* if this is equal to o, then \result is 0 *)&&(* if this is less than o, then \result is negative *)&&(* if this is greater than o, then \result is positive *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* o is not an instance of a comparable class *);
Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure
public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
     also
public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

equals

public boolean equals(nullable Object o)
Tell whether this integer is equal to the argument. Note that comparisons to BigIntegers are also handled.

Specified by:
equals in interface JMLType
Overrides:
equals in class Object
See Also:
compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: (class)pure
     also
public normal_behavior
requires o != null&&o instanceof org.jmlspecs.models.JMLInfiniteInteger;
{|
old org.jmlspecs.models.JMLInfiniteInteger n = (org.jmlspecs.models.JMLInfiniteInteger)o;
ensures \result <==> this.sign == n.sign&&this.is_infinite == n.is_infinite&&(!this.is_infinite&&!n.is_infinite ==> this.finite_value.compareTo(n.finite_value) == 0);
|}
     also
public normal_behavior
requires o != null&&o instanceof java.math.BigInteger;
{|
old java.math.BigInteger bi = (java.math.BigInteger)o;
ensures \result <==> !this.is_infinite&&this.finite_value.compareTo(bi) == 0;
|}
     also
public normal_behavior
requires o == null||!(o instanceof java.math.BigInteger||o instanceof org.jmlspecs.models.JMLInfiniteInteger);
ensures !\result ;
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 ;
Specifications inherited from overridden method equals(Object ob2) in interface JMLType:
       pure
     also
public normal_behavior
ensures \result ==> ob2 != null&&(* ob2 is not distinguishable from this, except by using mutation or == *);
    implies_that
public normal_behavior
{|
requires ob2 != null&&ob2 instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)ob2).equals(this) == \result ;
also
requires ob2 == this;
ensures \result <==> true;
|}

greaterThanOrEqualTo

public boolean greaterThanOrEqualTo(non_null JMLInfiniteInteger n)
Tell if this integer is greater than or equal to the argument.

See Also:
equals(Object), compareTo(Object), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: (class)pure
public normal_behavior
requires n != null;
ensures \result <==> (this.is_infinite ==> (this.nonnegative||(!n.nonnegative&&n.is_infinite)))&&(!this.is_infinite ==> ((n.is_infinite&&!n.nonnegative)||this.finite_value.compareTo(n.finite_value) >= 0));
    implies_that
public normal_behavior
requires n != null;
{|
requires (this.nonnegative&&this.is_infinite)||(!n.nonnegative&&n.is_infinite);
ensures \result ;
also
requires (n.nonnegative&&n.is_infinite)||(!this.nonnegative&&this.is_infinite);
ensures !\result ;
also
requires !this.is_infinite&&!n.is_infinite;
ensures \result <==> this.finite_value.compareTo(n.finite_value) >= 0;
|}

lessThanOrEqualTo

public boolean lessThanOrEqualTo(non_null JMLInfiniteInteger n)
Tell if this integer is less than or equal to the argument.

See Also:
equals(Object), compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: (class)pure
public normal_behavior
requires n != null;
ensures \result <==> n.greaterThanOrEqualTo(this);

greaterThan

public boolean greaterThan(non_null JMLInfiniteInteger n)
Tell if this integer is strictly greater than the argument.

See Also:
equals(Object), compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), lessThan(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: (class)pure
public normal_behavior
requires n != null;
ensures \result <==> !this.equals(n)&&this.greaterThanOrEqualTo(n);

lessThan

public boolean lessThan(non_null JMLInfiniteInteger n)
Tell if this integer is strictly less than the argument.

See Also:
equals(Object), compareTo(Object), greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), greaterThan(org.jmlspecs.models.JMLInfiniteInteger), lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: (class)pure
public normal_behavior
requires n != null;
ensures \result <==> !this.equals(n)&&this.lessThanOrEqualTo(n);

hashCode

public int hashCode()
Return a hash code for this integer.

Specified by:
hashCode in interface JMLType
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;
Specifications inherited from overridden method in interface JMLType:
       pure

abs

public JMLInfiniteInteger abs()
Return the absolute value of this integer.

See Also:
negate()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .nonnegative&&\result .is_infinite == this.is_infinite&&(!\result .is_infinite ==> \result .finite_value.equals(this.finite_value.abs()));

max

public JMLInfiniteInteger max(non_null JMLInfiniteInteger n)
Return the maximum of this integer and the argument.

See Also:
min(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null;
{|
requires this.greaterThanOrEqualTo(n);
ensures \result .equals(this);
also
requires n.greaterThanOrEqualTo(this);
ensures \result .equals(n);
|}

min

public JMLInfiniteInteger min(non_null JMLInfiniteInteger n)
Return the minimum of this integer and the argument.

See Also:
max(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null;
{|
requires this.lessThanOrEqualTo(n);
ensures \result .equals(this);
also
requires n.lessThanOrEqualTo(this);
ensures \result .equals(n);
|}

negate

public JMLInfiniteInteger negate()
Return the negation of this integer.

See Also:
abs(), subtract(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .sign == -1*this.sign;
     also
requires this.is_infinite;
ensures \result .is_infinite;
     also
requires !this.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.negate());

add

public JMLInfiniteInteger add(non_null JMLInfiniteInteger n)
Return the sum of this integer and the argument.

See Also:
subtract(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null;
{|
ensures \result != null;
also
requires this.is_infinite&&!n.is_infinite;
ensures \result .equals(this);
also
requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(n);
also
requires this.is_infinite&&n.is_infinite;
{|
requires this.nonnegative == n.nonnegative;
ensures \result .equals(this);
also
requires this.nonnegative != n.nonnegative;
ensures \result .equals(new java.math.BigInteger("0"));
|}
also
requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.add(n.finite_value));
|}

subtract

public JMLInfiniteInteger subtract(non_null JMLInfiniteInteger n)
Return the difference between this integer and the argument.

See Also:
add(org.jmlspecs.models.JMLInfiniteInteger), negate()
Specifications: non_null (class)pure
public normal_behavior
requires n != null;
{|
ensures \result != null;
also
requires this.is_infinite&&!n.is_infinite;
ensures \result .equals(this);
also
requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(n.negate());
also
requires this.is_infinite&&n.is_infinite;
{|
requires this.nonnegative == n.nonnegative;
ensures \result .equals(new java.math.BigInteger("0"));
also
requires this.nonnegative != n.nonnegative;
ensures \result .equals(this);
|}
also
requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.subtract(n.finite_value));
|}

multiply

public JMLInfiniteInteger multiply(non_null JMLInfiniteInteger n)
Return the product of this integer and the argument.

See Also:
divide(org.jmlspecs.models.JMLInfiniteInteger), remainder(org.jmlspecs.models.JMLInfiniteInteger), mod(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null;
{|
ensures \result != null&&\result .sign == this.sign*n.sign;
also
requires this.equals(new java.math.BigInteger("0"))||n.equals(new java.math.BigInteger("0"));
ensures \result .equals(new java.math.BigInteger("0"));
also
requires !(this.equals(new java.math.BigInteger("0"))||n.equals(new java.math.BigInteger("0")));
{|
requires this.is_infinite||n.is_infinite;
ensures \result .is_infinite;
also
requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.multiply(n.finite_value));
|}
|}

divide

public JMLInfiniteInteger divide(non_null JMLInfiniteInteger n)
                                   throws ArithmeticException
Return the quotient of this integer divided by the argument.

Throws:
ArithmeticException
See Also:
multiply(org.jmlspecs.models.JMLInfiniteInteger), remainder(org.jmlspecs.models.JMLInfiniteInteger), mod(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null&&n.sign != 0;
{|
ensures \result != null&&(\result .sign == 0||\result .sign == this.sign*n.sign);
also
requires this.is_infinite&&n.is_infinite;
ensures !\result .is_infinite&&\result .abs().equals(new java.math.BigInteger("1"));
also
requires this.is_infinite&&!n.is_infinite;
ensures \result .is_infinite;
also
requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(new java.math.BigInteger("0"));
also
requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.divide(n.finite_value));
|}
     also
public exceptional_behavior
requires n != null&&n.sign == 0;
signals_only java.lang.ArithmeticException;

remainder

public JMLInfiniteInteger remainder(non_null JMLInfiniteInteger n)
                                      throws ArithmeticException
Return the remainder of this integer divided by the argument.

Throws:
ArithmeticException
See Also:
divide(org.jmlspecs.models.JMLInfiniteInteger), mod(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null&&n.sign != 0;
{|
ensures \result != null;
also
requires this.is_infinite;
ensures \result .equals(new java.math.BigInteger("0"));
also
requires !this.is_infinite&&n.is_infinite;
ensures \result .abs().equals(this.abs());
ensures \result .sign == this.sign*n.sign;
also
requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.remainder(n.finite_value));
|}
     also
public exceptional_behavior
requires n != null&&n.sign == 0;
signals_only java.lang.ArithmeticException;

mod

public JMLInfiniteInteger mod(non_null JMLInfiniteInteger n)
                                throws ArithmeticException
Return this integer modulo the argument.

Throws:
ArithmeticException
See Also:
divide(org.jmlspecs.models.JMLInfiniteInteger), remainder(org.jmlspecs.models.JMLInfiniteInteger)
Specifications: non_null (class)pure
public normal_behavior
requires n != null&&n.sign == 1;
{|
ensures \result != null&&\result .sign >= 0;
also
requires this.is_infinite;
ensures \result .equals(new java.math.BigInteger("0"));
also
requires !this.is_infinite&&n.is_infinite;
ensures \result .equals(n);
also
requires !this.is_infinite&&!n.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.mod(n.finite_value));
|}
     also
public exceptional_behavior
requires n != null&&n.sign != 1;
signals_only java.lang.ArithmeticException;

pow

public JMLInfiniteInteger pow(int n)
                                throws ArithmeticException
Return this integer raised to the argument's power.

Throws:
ArithmeticException
Specifications: non_null (class)pure
public normal_behavior
requires n >= 0;
{|
ensures \result != null&&(\result .nonnegative <==> n%2 == 0||this.nonnegative);
also
requires this.is_infinite;
ensures n != 0 ==> \result .is_infinite;
ensures n == 0 ==> !\result .is_infinite&&\result .finite_value.equals(new java.math.BigInteger("1"));
also
requires !this.is_infinite;
ensures !\result .is_infinite&&\result .finite_value.equals(this.finite_value.pow(n));
|}
     also
public exceptional_behavior
requires n < 0;
signals_only java.lang.ArithmeticException;

doubleValue

public double doubleValue()
Return this integer approximated by a double.

See Also:
floatValue()
Specifications: (class)pure
public normal_behavior
requires this.is_infinite&&this.nonnegative;
ensures \result == Infinity;
     also
requires this.is_infinite&&!this.nonnegative;
ensures \result == -Infinity;
     also
requires !this.is_infinite;
ensures \result == this.finite_value.doubleValue();

floatValue

public float floatValue()
Return this integer approximated by a float.

See Also:
doubleValue()
Specifications: (class)pure
public normal_behavior
requires this.is_infinite&&this.nonnegative;
ensures \result == Infinity;
     also
requires this.is_infinite&&!this.nonnegative;
ensures \result == -Infinity;
     also
requires !this.is_infinite;
ensures \result == this.finite_value.floatValue();

toString

public String toString()
Return the decimal representation of this integer.

Overrides:
toString in class Object
See Also:
toString(int)
Specifications: (class)pure
     also
public normal_behavior
ensures \result .equals(this.toString(10));
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;

toString

public String toString(int radix)
Return the digits representing this integer in the given radix.

See Also:
toString()
Specifications: (class)pure
public model_program { ... }

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.