JML

org.jmlspecs.jmlrac.runtime
Class JMLOldExpressionCache

java.lang.Object
  extended byorg.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

Nested Class Summary
static class JMLOldExpressionCache.Key
          A class for representing keys for cache objects.
 
Field Summary
private  Map cache
          Map for (key, value) pairs.
 
Constructor Summary
JMLOldExpressionCache()
          Constructs a new, empty cache object.
 
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.

Constructor Detail

JMLOldExpressionCache

public JMLOldExpressionCache()
Constructs a new, empty cache object.

Method Detail

containsKey

public boolean containsKey(Object key)
Does this cache contain a value for the key, key?

 requires key != null;
 


containsKey

public boolean containsKey(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(Object key,
                Object value)
Puts the key/value pair to this cache.

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


put

public void put(Object[] key,
                Object value)
Puts the key/value pair to this cache.

 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.

 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.

 requires key != null;
 


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.