Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.translate
Class Substitute

    java.lang.Object
      escjava.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)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage