java.lang
Class Number

java.lang.Object
  java.lang.Number

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

BigDecimal, BigInteger, Byte, Double, Float, Integer, Long, NaturalNumber, Short

public abstract class Number

extends Object

implements Serializable

JML's specification of java.lang.Number.

Version:

$Revision: 1.7 $

Author:

Brandon Shilling, Gary T. Leavens

Class Specifications

Specifications inherited from class Object

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

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

Number()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
byte	byteValue()
abstract  double	doubleValue()
abstract  float	floatValue()
abstract  int	intValue()
abstract  long	longValue()
short	shortValue()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Constructor Detail

Number

public Number()

Specifications: pure

public normal_behavior
assignable objectState;

intValue

public abstract int intValue()

Specifications: pure

public normal_behavior
ensures (* \result is an int approximation to the value of this object *);

longValue

public abstract long longValue()

Specifications: pure

public normal_behavior
ensures (* \result is an long approximation to the value of this object *);

floatValue

public abstract float floatValue()

Specifications: pure

public normal_behavior
ensures (* \result is an float approximation to the value of this object *);

doubleValue

public abstract double doubleValue()

Specifications: pure

public normal_behavior
ensures (* \result is an double approximation to the value of this object *);

byteValue

public byte byteValue()

Specifications: pure

public normal_behavior
ensures (* \result is an byte approximation to the value of this object *);

shortValue

public short shortValue()

Specifications: pure

public normal_behavior
ensures (* \result is an short approximation to the value of this object *);