|
ESC/Java2 © 2003,2004,2005,2006 David Cok and Joseph Kiniry © 2005,2006 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 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. |
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)
|
| Uses of InitialState in escjava.vcGeneration |
| Methods in escjava.vcGeneration with parameters of type InitialState | |
abstract Expr |
ProverType.addTypeInfo(InitialState initState,
Expr tree)
This method is used by untyped prover logics to add typing predicates to the supplied VC term. |
| Uses of InitialState in escjava.vcGeneration.coq |
| Methods in escjava.vcGeneration.coq with parameters of type InitialState | |
Expr |
CoqProver.addTypeInfo(InitialState initState,
Expr tree)
|
| Uses of InitialState in escjava.vcGeneration.pvs |
| Methods in escjava.vcGeneration.pvs with parameters of type InitialState | |
Expr |
PvsProver.addTypeInfo(InitialState initState,
Expr tree)
|
| Uses of InitialState in escjava.vcGeneration.sammy |
| Methods in escjava.vcGeneration.sammy with parameters of type InitialState | |
Expr |
SammyProver.addTypeInfo(InitialState initState,
Expr tree)
|
| Uses of InitialState in escjava.vcGeneration.simplify |
| Methods in escjava.vcGeneration.simplify with parameters of type InitialState | |
Expr |
SimplifyProver.addTypeInfo(InitialState initState,
Expr tree)
|
| Uses of InitialState in escjava.vcGeneration.xml |
| Methods in escjava.vcGeneration.xml with parameters of type InitialState | |
Expr |
XmlProver.addTypeInfo(InitialState initState,
Expr tree)
At this stage, we do not know if the target prover is typed or not. |
|
ESC/Java2 © 2003,2004,2005,2006 David Cok and Joseph Kiniry © 2005,2006 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 | ||||||||||