org.jmlspecs.jml4.rac.runtime
Class JMLOldExpressionCache

java.lang.Object
  org.jmlspecs.jml4.rac.runtime.JMLOldExpressionCache

public class JMLOldExpressionCache
extends java.lang.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

Nested Class Summary

static class

JMLOldExpressionCache.Key A class for representing keys for cache objects.

Constructor Summary

JMLOldExpressionCache()
Constructs a new, empty cache object.

Method Summary

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

Methods inherited from class java.lang.Object

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

Constructor Detail

JMLOldExpressionCache

public JMLOldExpressionCache()

Constructs a new, empty cache object.

Method Detail

containsKey

public boolean containsKey(java.lang.Object key)

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

 requires key != null;
 

containsKey

public boolean containsKey(java.lang.Object[] key)

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

 requires key != null;
 

clear

public void clear()

Clears this cache.

put

public void put(java.lang.Object key,
                java.lang.Object value)

Puts the key/value pair to this cache.

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

put

public void put(java.lang.Object[] key,
                java.lang.Object value)

Puts the key/value pair to this cache.

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

get

public java.lang.Object get(java.lang.Object key)

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

 requires key != null;
 

get

public java.lang.Object get(java.lang.Object[] key)

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

 requires key != null;