org.jmlspecs.models
Class JMLPositiveInfinity

java.lang.Object
  org.jmlspecs.models.JMLInfiniteIntegerClass
      org.jmlspecs.models.JMLPositiveInfinity

All Implemented Interfaces:

Cloneable, Comparable, JMLComparable, JMLInfiniteInteger, JMLType, Serializable

public class JMLPositiveInfinity

extends JMLInfiniteIntegerClass

Positive Infinity.

Version:

$Revision: 1.16 $

Author:

Gary T. Leavens

See Also:

JMLNegativeInfinity

Class Specifications

public invariant_redundantly this.is_infinite; public invariant_redundantly this.sign == 1; public invariant_redundantly this.nonnegative; public represents is_infinite <- true; public represents sign <- 1;

Specifications inherited from class JMLInfiniteIntegerClass

public invariant this.owner == null;

Specifications inherited from class Object

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

Specifications inherited from interface JMLInfiniteInteger

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

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.models.JMLInfiniteInteger

finite_value, is_infinite, nonnegative, sign

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

JMLPositiveInfinity()           Initialize this object.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary
JMLInfiniteInteger	add(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.
int	compareTo(JMLInfiniteInteger n)           Compare this to the given integer, returning a comparison code.
JMLInfiniteInteger	divide(JMLInfiniteInteger n)           Return the quotient of this integer divided by the argument.
double	doubleValue()           Return this integer approximated by a double.
BigInteger	finiteValue()           Throw an ArithmeticException.
float	floatValue()           Return this integer approximated by a float.
int	hashCode()           Return a hash code for this object.
boolean	isFinite()           Return false.
JMLInfiniteInteger	mod(JMLInfiniteInteger n)           Return this integer modulo the argument.
JMLInfiniteInteger	multiply(JMLInfiniteInteger n)           Return the product of this integer and the argument.
JMLInfiniteInteger	negate()           Return negative infinity.
JMLInfiniteInteger	pow(int n)           Return this integer raised to the argument's power.
JMLInfiniteInteger	remainder(JMLInfiniteInteger n)           Return the remainder of this integer divided by the argument.
int	signum()           Return the sign of this integer.
JMLInfiniteInteger	subtract(JMLInfiniteInteger n)           Return the difference between this integer and the argument.
String	toString()           Return the string "Infinity".
String	toString(int radix)           Return the string "Infinity".

 

Methods inherited from class org.jmlspecs.models.JMLInfiniteIntegerClass

abs, clone, equals, greaterThan, greaterThanOrEqualTo, lessThan, lessThanOrEqualTo, max, min

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Constructor Detail

JMLPositiveInfinity

public JMLPositiveInfinity()

Initialize this object.

Specifications: (class)pure

signum

public int signum()

Return the sign of this integer.

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (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()

Return false.

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

public normal_behavior
ensures \result == !this.is_infinite;

finiteValue

public BigInteger finiteValue()
                       throws ArithmeticException

Throw an ArithmeticException.

Throws:

ArithmeticException

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)

Compare this to the given integer, returning a comparison code.

Specifications: (class)pure

Specifications inherited from overridden method in class JMLInfiniteIntegerClass:
       (class)pure

Specifications inherited from overridden method compareTo(Object o) in interface JMLInfiniteInteger:
       (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);

compareTo

public int compareTo(non_null Object o)
              throws ClassCastException

Compare this to o, returning a comparison code.

Parameters:

o - the object this is compared to.

Throws:

ClassCastException - when o is not a JMLInfiniteInteger or a BigInteger.

See Also:

JMLInfiniteInteger.equals(Object), JMLInfiniteInteger.greaterThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.greaterThan(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.lessThanOrEqualTo(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.lessThan(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method compareTo(Object o) in interface JMLInfiniteInteger:
       (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);

hashCode

public int hashCode()

Return a hash code for this object.

Specified by:

hashCode in interface JMLInfiniteInteger

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 JMLInfiniteInteger:
       (class)pure

Specifications inherited from overridden method in interface JMLType:
       pure

negate

public JMLInfiniteInteger negate()

Return negative infinity.

See Also:

JMLInfiniteInteger.abs(), JMLInfiniteInteger.subtract(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)

Return the sum of this integer and the argument.

See Also:

JMLInfiniteInteger.subtract(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method add(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)

Return the difference between this integer and the argument.

See Also:

JMLInfiniteInteger.add(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.negate()

Specifications: (class)pure

Specifications inherited from overridden method subtract(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)

Return the product of this integer and the argument.

See Also:

JMLInfiniteInteger.divide(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.remainder(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.mod(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method multiply(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)
                          throws ArithmeticException

Return the quotient of this integer divided by the argument.

Throws:

ArithmeticException

See Also:

JMLInfiniteInteger.multiply(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.remainder(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.mod(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method divide(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)
                             throws ArithmeticException

Return the remainder of this integer divided by the argument.

Throws:

ArithmeticException

See Also:

JMLInfiniteInteger.divide(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.mod(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method remainder(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       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(JMLInfiniteInteger n)
                       throws ArithmeticException

Return this integer modulo the argument.

Throws:

ArithmeticException

See Also:

JMLInfiniteInteger.divide(org.jmlspecs.models.JMLInfiniteInteger), JMLInfiniteInteger.remainder(org.jmlspecs.models.JMLInfiniteInteger)

Specifications: (class)pure

Specifications inherited from overridden method mod(JMLInfiniteInteger n) in interface JMLInfiniteInteger:
       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: (class)pure

Specifications inherited from overridden method pow(int n) in interface JMLInfiniteInteger:
       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:

JMLInfiniteInteger.floatValue()

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (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:

JMLInfiniteInteger.doubleValue()

Specifications: (class)pure

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (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 string "Infinity".

Specified by:

toString in interface JMLInfiniteInteger

Overrides:

toString in class Object

See Also:

JMLInfiniteInteger.toString(int)

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;

Specifications inherited from overridden method in interface JMLInfiniteInteger:
       (class)pure

     also

public normal_behavior
ensures \result .equals(this.toString(10));

toString

public String toString(int radix)

Return the string "Infinity".

See Also:

JMLInfiniteInteger.toString()

Specifications: (class)pure

Specifications inherited from overridden method toString(int radix) in interface JMLInfiniteInteger:
       (class)pure

public model_program { ... }