JML

org.jmlspecs.models
Class JMLFiniteInteger

java.lang.Object
  extended byorg.jmlspecs.models.JMLInfiniteIntegerClass
      extended byorg.jmlspecs.models.JMLFiniteInteger
All Implemented Interfaces:
Cloneable, Comparable, JMLComparable, JMLInfiniteInteger, JMLType, Serializable

public class JMLFiniteInteger
extends JMLInfiniteIntegerClass

Arbitrary precision integers with a finite value.

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

Class Specifications
public invariant !this.is_infinite;
protected represents finite_value <- this.val;
protected represents sign <- this.val.signum();
protected represents is_infinite <- false;

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
 
Field Summary
static JMLFiniteInteger ONE
          The number one (1).
protected  BigInteger val
           
static JMLFiniteInteger ZERO
          The number zero (0).
 
Constructor Summary
JMLFiniteInteger()
          Initialize this finite integer to zero (0).
JMLFiniteInteger(non_null BigInteger n)
          Initialize this finite integer from the given BigInteger.
JMLFiniteInteger(long n)
          Initialize this finite integer from the given long.
 
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()
          Return the value of this integer.
 float floatValue()
          Return this integer approximated by a float.
 int hashCode()
          Return a hash code for this object.
 int intValue()
          Converts this BigInteger to an integer
 boolean isFinite()
          Return true.
 long longValue()
          Converts this BigInteger to a long
 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 the negation of this integer.
 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 decimal representation of this integer.
 String toString(int radix)
          Return the digits representing this integer in the given radix.
 
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
 

Field Detail

val

protected final BigInteger val
Specifications: non_null
is in groups: sign finite_value is_infinite

ZERO

public static final JMLFiniteInteger ZERO
The number zero (0).


ONE

public static final JMLFiniteInteger ONE
The number one (1).

Constructor Detail

JMLFiniteInteger

public JMLFiniteInteger()
Initialize this finite integer to zero (0).

Specifications: (class)pure
public normal_behavior
assignable nonnegative, sign, is_infinite, finite_value;
ensures !this.is_infinite;
ensures this.finite_value.equals(java.math.BigInteger.ZERO);
     also
private normal_behavior
assignable val;

JMLFiniteInteger

public JMLFiniteInteger(non_null BigInteger n)
                 throws IllegalArgumentException
Initialize this finite integer from the given BigInteger.

Throws:
IllegalArgumentException
Specifications: (class)pure
public behavior
assignable nonnegative, sign, is_infinite, finite_value;
ensures !this.is_infinite&&this.finite_value.equals(n);
signals_only java.lang.IllegalArgumentException;
signals (java.lang.IllegalArgumentException) n == null;

JMLFiniteInteger

public JMLFiniteInteger(long n)
Initialize this finite integer from the given long.

Specifications: (class)pure
Method Detail

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

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()
Return the value of this integer.

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 NullPointerException,
                     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.
NullPointerException
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 the negation of this integer.

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)
Return the quotient of this integer divided by the argument.

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)
Return the remainder of this integer divided by the argument.

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)
Return this integer raised to the argument's power.

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 decimal representation of this integer.

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 digits representing this integer in the given radix.

See Also:
JMLInfiniteInteger.toString()
Specifications: (class)pure
Specifications inherited from overridden method toString(int radix) in interface JMLInfiniteInteger:
       (class)pure
public model_program { ... }

longValue

public long longValue()
Converts this BigInteger to a long

Specifications: (class)pure

intValue

public int intValue()
Converts this BigInteger to an integer

Specifications: (class)pure

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.