org.jmlspecs.jmlrac.runtime
Class JMLOldExpressionCache

java.lang.Object
  org.jmlspecs.jmlrac.runtime.JMLOldExpressionCache

public class JMLOldExpressionCache

extends Object

An abstraction of caches for JML old expressions. This class implements a simple map that is suitable for storing the values of old expressions evaluated in the pre-state. If an old expression appears in a quantifier, we can view it as a mapping from quantified (bound) variables to values. An object of this class is used to store this mapping.

Version:

$Revision: 1.3 $

Author:

Yoonsik Cheon

Class Specifications

Specifications inherited from class Object

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

Nested Class Summary
static class	JMLOldExpressionCache.Key           A class for representing keys for cache objects.

 

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

 

Field Summary
private  Map	cache           Map for (key, value) pairs.

 

Constructor Summary

JMLOldExpressionCache()           Constructs a new, empty cache object.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	clear()           Clears this cache.
boolean	containsKey(Object key)           Does this cache contain a value for the key, key?
boolean	containsKey(Object[] key)           Does this cache contain a value for the key, key?
Object	get(Object key)           Returns the value for the key, key.
Object	get(Object[] key)           Returns the value for the key, key.
void	put(Object key, Object value)           Puts the key/value pair to this cache.
void	put(Object[] key, Object value)           Puts the key/value pair to this cache.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

cache

private Map cache

Map for (key, value) pairs.

Specifications: non_null

JMLOldExpressionCache

public JMLOldExpressionCache()

Constructs a new, empty cache object.

containsKey

public boolean containsKey(Object key)

Does this cache contain a value for the key, key?

Specifications:

requires key != null;

containsKey

public boolean containsKey(Object[] key)

Does this cache contain a value for the key, key?

Specifications:

requires key != null;

clear

public void clear()

Clears this cache.

put

public void put(Object key,
                Object value)

Puts the key/value pair to this cache.

Specifications:

requires key != null&&value != null;

put

public void put(Object[] key,
                Object value)

Puts the key/value pair to this cache.

Specifications:

requires key != null&&value != null;

get

public Object get(Object key)

Returns the value for the key, key. If no value is found for the given key, null is returned.

Specifications:

requires key != null;

get

public Object get(Object[] key)

Returns the value for the key, key. If no value is found for the given key, null is returned.

Specifications:

requires key != null;