JML

java.lang
Class Byte

java.lang.Object
  extended byjava.lang.Number
      extended byjava.lang.Byte
All Implemented Interfaces:
Comparable, Serializable

public final class Byte
extends Number
implements Comparable

JML's specification of java.lang.Byte.

Version:
$Revision: 1.20 $
Author:
Brandon Shilling, Gary T. Leavens

Class Specifications
represents theByte <- this.byteValue();

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
 byte theByte
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
static byte MAX_VALUE
           
static byte MIN_VALUE
           
static Class TYPE
           
 
Constructor Summary
Byte(byte value)
           
Byte(String s)
           
 
Model Method Summary
static boolean decodeable(String nm)
           
static boolean parseable(String s)
           
static boolean parseable(String s, int r)
           
 
Model methods inherited from class java.lang.Object
hashValue
 
Model methods inherited from interface java.lang.Comparable
definedComparison, sgn
 
Method Summary
 byte byteValue()
           
 int compareTo(non_null Byte anotherByte)
           
 int compareTo(non_null Object o)
           
static Byte decode(String nm)
           
 double doubleValue()
           
 boolean equals(nullable Object obj)
           
 float floatValue()
           
 int hashCode()
           
 int intValue()
           
 long longValue()
           
static byte parseByte(String s)
           
static byte parseByte(String s, int radix)
           
 short shortValue()
           
 String toString()
           
static String toString(byte b)
           
static Byte valueOf(String s)
           
static Byte valueOf(String s, int radix)
           
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Model Field Detail

theByte

public byte theByte
Field Detail

MIN_VALUE

public static final byte MIN_VALUE

MAX_VALUE

public static final byte MAX_VALUE

TYPE

public static final Class TYPE
Specifications: non_null
Constructor Detail

Byte

public Byte(byte value)
Specifications: (class)pure
public normal_behavior
assignable theByte;
ensures this.theByte == value;

Byte

public Byte(String s)
     throws NumberFormatException
Throws:
NumberFormatException
Specifications: (class)pure
public normal_behavior
requires parseable(s);
assignable theByte;
ensures this.theByte == parseByte(s);
     also
public exceptional_behavior
requires !parseable(s);
assignable \nothing;
signals (java.lang.NumberFormatException) true;
Model Method Detail

parseable

public static boolean parseable(String s,
                                int r)
Specifications: pure
public normal_behavior
requires 2 <= r&&r <= 36;
assignable \nothing;
ensures \result <==> s != null&&!s.equals("")&&( \forall int i; 0 <= i&&i < s.length(); java.lang.Character.digit(s.charAt(i),r) != -1);
     also
public normal_behavior
requires 2 <= r&&r <= 36;
assignable \nothing;
ensures \result <==> s != null&&!s.equals("")&&( \forall int i; 1 <= i&&i < s.length()&&s.charAt(0) == 45; java.lang.Character.digit(s.charAt(i),r) != -1);

parseable

public static boolean parseable(String s)
Specifications: pure
public normal_behavior
assignable \nothing;
ensures \result == parseable(s,10);

decodeable

public static boolean decodeable(String nm)
Specifications: pure
public normal_behavior
{|
requires nm != null&&nm.substring(0,2).equalsIgnoreCase("0x");
ensures \result == parseable(nm.substring(2),16);
also
requires nm != null&&nm.substring(0,3).equalsIgnoreCase("-0x");
ensures \result == parseable(nm.substring(3),16);
also
requires nm.startsWith("#");
ensures \result == parseable(nm.substring(1),16);
also
requires nm.startsWith("-#");
ensures \result == parseable(nm.substring(2),16);
also
requires nm.startsWith("O");
ensures \result == parseable(nm.substring(1),8);
also
requires nm.startsWith("-O");
ensures \result == parseable(nm.substring(2),8);
also
ensures \result == parseable(nm);
|}
Method Detail

toString

public static String toString(byte b)
Specifications: pure non_null
public normal_behavior
{|
requires b < 0;
assignable \nothing;
ensures \result .charAt(0) == 45&&\result .charAt(1) != 48&&b == parseByte(\result );
also
requires b > 0;
assignable \nothing;
ensures \result != null&&\result .charAt(0) != 48&&b == parseByte(\result );
also
requires b == 0;
assignable \nothing;
ensures "0".equals(\result );
|}
    implies_that
public normal_behavior
ensures (*\result is a string representation of s *);
    for_example
public normal_example
requires b == -34;
ensures "-34".equals(\result );

parseByte

public static byte parseByte(String s)
                      throws NumberFormatException
Throws:
NumberFormatException
Specifications: pure
public normal_behavior
requires parseable(s);
assignable \nothing;
ensures \result == parseByte(s,10);
     also
public exceptional_behavior
requires !parseable(s);
assignable \nothing;
signals_only java.lang.NumberFormatException;

parseByte

public static byte parseByte(String s,
                             int radix)
                      throws NumberFormatException
Throws:
NumberFormatException
Specifications: pure
public normal_behavior
requires parseable(s,radix);
assignable \nothing;
ensures (* the byte represented by string s with specified radix *);
     also
public exceptional_behavior
requires !parseable(s,radix);
assignable \nothing;
signals_only java.lang.NumberFormatException;
    for_example
public normal_example
requires s.equals("-34")&&radix == 10;
ensures \result == -34;

valueOf

public static Byte valueOf(String s,
                           int radix)
                    throws NumberFormatException
Throws:
NumberFormatException
Specifications: pure non_null
public normal_behavior
requires parseable(s,radix);
assignable \nothing;
ensures \fresh(\result );
ensures \result .byteValue() == parseByte(s,radix);
     also
public exceptional_behavior
requires !parseable(s,radix);
assignable \nothing;
signals_only java.lang.NumberFormatException;

valueOf

public static Byte valueOf(String s)
                    throws NumberFormatException
Throws:
NumberFormatException
Specifications: pure non_null
public normal_behavior
requires parseable(s);
assignable \nothing;
ensures \fresh(\result );
ensures \result .byteValue() == parseByte(s);
     also
public exceptional_behavior
requires !parseable(s);
assignable \nothing;
signals_only java.lang.NumberFormatException;

decode

public static Byte decode(String nm)
                   throws NumberFormatException
Throws:
NumberFormatException
Specifications: pure non_null
public normal_behavior
requires decodeable(nm);
assignable \nothing;
ensures (* \result is a Byte representation of nm *);
     also
public exceptional_behavior
requires !decodeable(nm);
assignable \nothing;
signals (java.lang.NumberFormatException) true;

byteValue

public byte byteValue()
Overrides:
byteValue in class Number
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures \result == this.theByte;
Specifications inherited from overridden method in class Number:
       pure
public normal_behavior
ensures (* \result is an byte approximation to the value of this object *);

shortValue

public short shortValue()
Overrides:
shortValue in class Number
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures \result == this.theByte;
Specifications inherited from overridden method in class Number:
       pure
public normal_behavior
ensures (* \result is an short approximation to the value of this object *);

intValue

public int intValue()
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures \result == this.theByte;
Specifications inherited from overridden method in class Number:
       pure
public normal_behavior
ensures (* \result is an int approximation to the value of this object *);

longValue

public long longValue()
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures \result == this.theByte;
Specifications inherited from overridden method in class Number:
       pure
public normal_behavior
ensures (* \result is an long approximation to the value of this object *);

floatValue

public float floatValue()
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures \result == this.theByte;
Specifications inherited from overridden method in class Number:
       pure
public normal_behavior
ensures (* \result is an float approximation to the value of this object *);

doubleValue

public double doubleValue()
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures \result == this.theByte;
Specifications inherited from overridden method in class Number:
       pure
public normal_behavior
ensures (* \result is an double approximation to the value of this object *);

toString

public String toString()
Overrides:
toString in class Object
Specifications: non_null (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;

hashCode

public int hashCode()
Overrides:
hashCode in class Object
Specifications: (class)pure
     also
public normal_behavior
assignable \nothing;
ensures (* \result is a hash code for this object *);
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;

equals

public boolean equals(nullable Object obj)
Overrides:
equals in class Object
Specifications: pure
     also
public normal_behavior
{|
requires obj != null&&(obj instanceof java.lang.Byte);
assignable \nothing;
ensures \result == (this.theByte == ((java.lang.Byte)obj).byteValue());
also
requires obj == null||!(obj instanceof java.lang.Byte);
assignable \nothing;
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 ;

compareTo

public int compareTo(non_null Byte anotherByte)
Specifications: pure
public normal_behavior
requires anotherByte != null;
{|
requires this.theByte == anotherByte.byteValue();
assignable \nothing;
ensures \result == 0;
also
requires this.theByte < anotherByte.byteValue();
assignable \nothing;
ensures \result < 0;
also
requires this.theByte > anotherByte.byteValue();
assignable \nothing;
ensures \result > 0;
|}
     also
public exceptional_behavior
requires anotherByte == null;
assignable \nothing;
signals (java.lang.NullPointerException) true;
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)
Specified by:
compareTo in interface Comparable
Specifications: pure
     also
public normal_behavior
requires o != null&&(o instanceof java.lang.Byte);
assignable \nothing;
ensures \result == this.compareTo((java.lang.Byte)o);
     also
public exceptional_behavior
requires o != null&&!(o instanceof java.lang.Byte);
assignable \nothing;
signals (java.lang.ClassCastException) true;
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);

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.