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

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