org.jmlspecs.models
Class JMLNullSafe

java.lang.Object
  org.jmlspecs.models.JMLNullSafe

public class JMLNullSafe

extends Object

A class with static methods that safely work with null objects.

Version:

$Revision: 1.8 $

Author:

Katie Becker and 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
private	JMLNullSafe()           No instances of this class can be created.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static boolean	equals(nullable Object o1, nullable Object o2)           Test for equality of o1 and o2, allowing either to be null.
static int	hashCode(nullable Object o)
static String	toString(nullable Object o)

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

JMLNullSafe

private JMLNullSafe()

No instances of this class can be created.

equals

public static boolean equals(nullable Object o1,
                             nullable Object o2)

Test for equality of o1 and o2, allowing either to be null.

Specifications: pure

ensures \result <==> (o1 == null ? o2 == null : o1.equals(o2));

toString

public static String toString(nullable Object o)

Specifications:

public normal_behavior
requires o == null;
assignable \nothing;
ensures \result != null&&\result .equals("null");

     also

requires o != null;
ensures \result != null;

     also

public model_program { ... }

hashCode

public static int hashCode(nullable Object o)

Specifications:

public normal_behavior
requires o == null;
assignable \nothing;
ensures \result == 0;

     also

public model_program { ... }