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.ast.Spec

Packages that use Spec
escjava.ast |
escjava.translate |

Uses of Spec in escjava.ast

Fields in escjava.ast declared as Spec
`Spec` | `Call.spec`

Methods in escjava.ast that return Spec
`static Spec` | `Spec.make(DerivedMethodDecl dmd, ExprVec targets, ExprVec specialTargets, java.util.Hashtable preVarMap, ExprVec preAssumptions, ConditionVec pre, ExprVec postAssumptions, ConditionVec post, boolean modifiesEverything, java.util.Set postconditionLocations)`

Methods in escjava.ast with parameters of type Spec
`abstract java.lang.Object` | `VisitorArgResult.visitSpec(Spec x, java.lang.Object o)`
`abstract void` | `Visitor.visitSpec(Spec x)`
`void` | `EscPrettyPrint.printSpec(java.io.OutputStream o, int ind, Spec spec)`

Uses of Spec in escjava.translate

Methods in escjava.translate that return Spec
`static Spec` | `GetSpec.getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)`
`static Spec` | `GetSpec.getSpecForInline(RoutineDecl rd, FindContributors scope)`
`static Spec` | `GetSpec.getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)`
`private static Spec` | `GetSpec.getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)`
`private static Spec` | `GetSpec.trMethodDecl(DerivedMethodDecl dmd, java.util.Hashtable premap)` Translates a MethodDecl to a Spec.
`private static Spec` | `GetSpec.extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs)` Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
`private static Spec` | `GetSpec.extendSpecForBody(Spec spec, FindContributors scope, Set synTargs)` Implements ExtendSpecForBody, section 7.4 of ESCJ 16.

Methods in escjava.translate with parameters of type Spec
`private static Spec` | `GetSpec.extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs)` Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
`private static Spec` | `GetSpec.extendSpecForBody(Spec spec, FindContributors scope, Set synTargs)` Implements ExtendSpecForBody, section 7.4 of ESCJ 16.
`private static void` | `GetSpec.addInvariantBody(InvariantInfo ii, Spec spec, Set synTargs)` Extend `spec`, in a way appropriate for checking the body of a method or constructor, to account for invariant `ii.J` declared in class `ii.U`.
`private static ParamAndGlobalVarInfo` | `GetSpec.collectParamsAndGlobals(Spec spec, FindContributors scope)` Collects the parameters of `spec.args` and the static fields in `scope`, whose types are class types.
`static GuardedCmd` | `GetSpec.surroundBodyBySpec(GuardedCmd body, Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int locEndCurlyBrace)` Returns a command that first does an `assume` for each precondition in `spec`, then does `body`, then checks the postconditions of `spec`, and finally checks the modifies constraints implied by `spec`.
`private static void` | `GetSpec.checkModifiesConstraints(Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int loc, StackVector code)`

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