ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

escjava.translate
Class Substitute

java.lang.Object
  extended byescjava.translate.Substitute

public class Substitute
extends java.lang.Object

Responsible for performing substitutions in expressions.


Nested Class Summary
private static class Substitute.SetRef
           
 
Field Summary
static Expr resexpr
           
static Expr thisexpr
           
 
Constructor Summary
Substitute()
           
 
Method Summary
static Expr doSimpleSubst(java.util.Hashtable subst, Expr e)
           
static Expr doSubst(java.util.Hashtable subst, Expr e)
          Does substitution on GCExprs union (resolved) SpecExprs.
private static Expr doSubst(java.util.Hashtable subst, Expr e, Substitute.SetRef rhsVars)
          Does substitution on GCExprs union (resolved) SpecExprs.
static Set freeVars(ASTNode e)
          Calculate the free variables of an expression or a GuardedCmd.
static boolean mentionsFresh(Expr e)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

resexpr

public static final Expr resexpr

thisexpr

public static final Expr thisexpr
Constructor Detail

Substitute

public Substitute()
Method Detail

doSubst

public static Expr doSubst(java.util.Hashtable subst,
                           Expr e)
Does substitution on GCExprs union (resolved) SpecExprs.

No SubstExpr's may be contained in e.


doSimpleSubst

public static Expr doSimpleSubst(java.util.Hashtable subst,
                                 Expr e)

doSubst

private static Expr doSubst(java.util.Hashtable subst,
                            Expr e,
                            Substitute.SetRef rhsVars)
Does substitution on GCExprs union (resolved) SpecExprs.

No SubstExpr's may be contained in e.

rhsVars refers to a pointer to a Set. This pointer is either null or the set of variables (GenericVarDecl's) occurring in right-hand sides of subst.


freeVars

public static Set freeVars(ASTNode e)
Calculate the free variables of an expression or a GuardedCmd.

Precondition; e must be resolved, e may not contain FieldAccess as a subnode.

[mdl: I have checked that this code works with invariants translated to Exprs. I am unsure if it works correctly on anything else.] Note: length is not a free variable of translated code. (It turns into applications of the built-in function arrayLength.)


mentionsFresh

public static boolean mentionsFresh(Expr e)

ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage