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 InitialState

    java.lang.Object
      escjava.translate.InitialState

public final class InitialState
extends java.lang.Object

This class provides two methods used in the generation of a verification condition for a method or constructor (see section 8 of ESCJ 16).

Field Summary
`private Expr` | `is`
`private java.util.Hashtable` | `premap`

Constructor Summary
`InitialState(FindContributors scope)`

Method Summary
`private VariableAccess` | `addMapping(GenericVarDecl vd)`
`Expr` | `getInitialState()`
`java.util.Hashtable` | `getPreMap()`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### premap

    private java.util.Hashtable premap

### is

    private Expr is

Constructor Detail

### InitialState

    public InitialState(FindContributors scope)

Method Detail

### addMapping

    private VariableAccess addMapping(GenericVarDecl vd)

### getPreMap

    public java.util.Hashtable getPreMap()

### getInitialState

    public Expr getInitialState()

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