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 NEXT | FRAMES NO FRAMES

## Uses of Class
escjava.translate.InitialState

Packages that use InitialState
escjava |
escjava.gui |
escjava.pa |

Uses of InitialState in escjava

Methods in escjava with parameters of type InitialState
`private void` | `Main.processTypeDeclElem(TypeDeclElem te, TypeSig sig, InitialState initState)` Run stages 3+..6 as requested on a TypeDeclElem.
`private java.lang.String` | `Main.processRoutineDecl(RoutineDecl r, TypeSig sig, InitialState initState)` Run stages 3+..6 as requested on a RoutineDeclElem; returns a short (~ 1 word) status message.
`protected GuardedCmd` | `Main.computeBody(RoutineDecl r, InitialState initState)` This method computes the guarded command (including assuming the precondition, the translated body, the checked postcondition, and the modifies constraints) for the method or constructor `r` in scope `scope`.

Uses of InitialState in escjava.gui

Fields in escjava.gui declared as InitialState
`InitialState` | `GUI.TDTreeValue.initState`

Uses of InitialState in escjava.pa

Methods in escjava.pa with parameters of type InitialState
`static void` | `Traverse.compute(GuardedCmd g, InitialState initState, Translate tr)`

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 NEXT | FRAMES NO FRAMES

The ESC/Java2 Project Homepage