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 GetSpec

    java.lang.Object
      escjava.translate.GetSpec

public final class GetSpec
extends java.lang.Object

Responsible for getting Spec for calls. Includes ... from ESCJ16c.

Field Summary
`private static java.util.HashSet` | `collectInvariantsAxsToAdd` Collects the invariants in `scope`.
`private static ASTDecoration` | `dmdDecoration`
`private static ASTDecoration` | `nonnullDecoration` * Decorates `GenericVarDecl`'s to point to * NonNullPragmas (SimpleModifierPragma's).

Constructor Summary
`GetSpec()`

Method Summary
`private static void` | `addAssumptions(ExprVec ev, StackVector code)` Appends `code` with an `assume C` command for every condition `C` in `cv`.
`static void` | `addAxioms(java.util.Set axsToAdd, ExprVec assumptions)` axsToAdd holds a Set of RepHelper - we need to add to the assumptions any axioms pertinent to the RepHelper.
`static ConditionVec` | `addConstraintClauses(ConditionVec post, TypeDecl decl, java.util.Hashtable wt, ExprVec postAssumptions)`
`private static void` | `addFreeTypeCorrectAs(GenericVarDecl vd, Type type, ConditionVec cv)` Adds to `cv` a condition stating that `vd` has type `type`.
`private static void` | `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 void` | `addModifiersToDMD(DerivedMethodDecl dmd, RoutineDecl rd)` * Add the modifiers of rd to dmd, making any necessary substitions * of parameter names.
`private static ExprVec` | `addNewAxs(java.util.HashSet axsToAdd, ExprVec assumptions)`
`private static void` | `addSuperInterfaces(TypeDecl td, Set set)`
`private static void` | `assumeConditions(ConditionVec cv, StackVector code)`
`private static void` | `checkConditions(ConditionVec cv, int loc, StackVector code)` Appends `code` with an `check loc: C` command for every condition `C` in `cv`.
`private static void` | `checkModifiesConstraints(Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int loc, StackVector code)`
`private static ExprVec` | `collectAxioms(FindContributors scope)` Collects the axioms in `scope`.
`static void` | `collectFields(Expr e, java.util.Set s)`
`private static InvariantInfo` | `collectInvariants(FindContributors scope, java.util.Hashtable premap)`
`private static ParamAndGlobalVarInfo` | `collectParamsAndGlobals(Spec spec, FindContributors scope)` Collects the parameters of `spec.args` and the static fields in `scope`, whose types are class types.
`(package private) static VariableAccess` | `createVarVariant(GenericVarDecl vd, java.lang.String postfix)` * Given a GenericVarDecl named "x@old", returns a VariableAccess to a * fresh LocalVarDecl named "x@ ". * * This handles ESCJ 23b case 13.
`private static CondExprModifierPragma` | `doSubst(java.util.Hashtable subst, CondExprModifierPragma emp)` Perform a substitution on a CondExprModifierPragma *
`private static ExprModifierPragma` | `doSubst(java.util.Hashtable subst, ExprModifierPragma emp)` Perform a substitution on an ExprModifierPragma *
`private static VarExprModifierPragma` | `doSubst(java.util.Hashtable subst, VarExprModifierPragma vemp)` Perform a substitution on a VarExprModifierPragma *
`private static boolean` | `exprIsVisible(TypeSig originType, Expr e)`
`private static Spec` | `extendSpecForBody(Spec spec, FindContributors scope, Set synTargs)` Implements ExtendSpecForBody, section 7.4 of ESCJ 16.
`private static Spec` | `extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs)` Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
`private static ExprModifierPragmaVec` | `filterExprModPragmas(ExprModifierPragmaVec vec, FindContributors scope)`
`static DerivedMethodDecl` | `filterMethodDecl(DerivedMethodDecl dmd, FindContributors scope)`
`private static ModifiesGroupPragmaVec` | `filterModifies(ModifiesGroupPragmaVec mvec, FindContributors scope)`
`private static VarExprModifierPragmaVec` | `filterVarExprModPragmas(VarExprModifierPragmaVec vec, FindContributors scope)`
`static DerivedMethodDecl` | `getCombinedMethodDecl(RoutineDecl rd)` * Implement GetCombinedMethodDecl from ESCJ 16c section 7: * * Precondition: the type declaring rd has been typechecked.
`private static Spec` | `getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)`
`static java.util.Enumeration` | `getFirstInheritedInterfaces(ClassDecl cd)`
`static TypeDeclElemVec` | `getRepresentsClauses(TypeDecl td, FieldDecl fd)` Gets the represents clauses for a model field fd as seen from a type declaration td; fd may be declared in td or in a supertype of td.
`static Spec` | `getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)`
`static Spec` | `getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)`
`static Spec` | `getSpecForInline(RoutineDecl rd, FindContributors scope)`
`(package private) static java.util.Hashtable` | `makeSubst(java.util.Enumeration e, java.lang.String postfix)` Converts a GenericVarDecl enumeration to a mapping from those variables to new Variableaccesses.
`(package private) static java.util.Hashtable` | `makeSubst(FormalParaDeclVec args, java.lang.String postfix)`
`private static InvariantInfo` | `mergeInvariants(InvariantInfo ii)`
`private static void` | `nonNullInitChecks(TypeDecl td, ConditionVec post)` Add to `post` all NonNullInit checks for non_null instance fields and instance ghost fields declared in `td`.
`static SimpleModifierPragma` | `NonNullPragma(GenericVarDecl v)` * Has a particular declaration been declared non_null?
`(package private) static java.util.Hashtable` | `restrict(java.util.Hashtable map, java.util.Enumeration e)` Creates and returns a new map that is `map` restricted to the domain `e`.
`private static void` | `setNonNullPragma(GenericVarDecl v, SimpleModifierPragma nonnull)` * Mark v as non_null because of non_null pragma nonnull. * * Precondition: nonnull is a NON_NULL pragma. * * (Used to implement inheritence of non_null's.)
`private static VariableAccess` | `shave(Expr e)` Shaves a GC designator.
`static SimpleModifierPragma` | `superNonNullPragma(GenericVarDecl v)` Returns non-null if the formal parameter is declared non-null in some overridden declaration of the method.
`static GuardedCmd` | `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 Spec` | `trMethodDecl(DerivedMethodDecl dmd, java.util.Hashtable premap)` Translates a MethodDecl to a Spec.
`private static ConditionVec` | `trMethodDeclPostcondition(DerivedMethodDecl dmd, java.util.Hashtable wt, ExprVec postAssumptions)` Computes the postconditions, according to section 7.2.2 of ESCJ 16.
`private static ConditionVec` | `trMethodDeclPreconditions(DerivedMethodDecl dmd, ExprVec preAssumptions)` Computes the preconditions, according to section 7.2.0 of ESCJ 16.

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

Field Detail

### dmdDecoration

    private static ASTDecoration dmdDecoration

### collectInvariantsAxsToAdd

    private static java.util.HashSet collectInvariantsAxsToAdd

  Collects the invariants in `scope`.

### nonnullDecoration

    private static ASTDecoration nonnullDecoration

  * Decorates `GenericVarDecl`'s to point to * NonNullPragmas (SimpleModifierPragma's).

Constructor Detail

### GetSpec

    public GetSpec()

Method Detail

### getSpecForCall

    public static Spec getSpecForCall(RoutineDecl rd,
                                      FindContributors scope,
                                      Set predictedSynTargs)

### getSpecForInline

    public static Spec getSpecForInline(RoutineDecl rd,
                                        FindContributors scope)

### getSpecForBody

    public static Spec getSpecForBody(RoutineDecl rd,
                                      FindContributors scope,
                                      Set synTargs,
                                      java.util.Hashtable premap)

### getCommonSpec

    private static Spec getCommonSpec(RoutineDecl rd,
                                      FindContributors scope,
                                      java.util.Hashtable premap)

### getCombinedMethodDecl

    public static DerivedMethodDecl getCombinedMethodDecl(RoutineDecl rd)

  * Implement GetCombinedMethodDecl from ESCJ 16c section 7:

  * * Precondition: the type declaring rd has been typechecked.

  * * Note: this routine may typecheck the supertypes of the type that * declares rd.

### addModifiersToDMD

    private static void addModifiersToDMD(DerivedMethodDecl dmd,
                                          RoutineDecl rd)

  * Add the modifiers of rd to dmd, making any necessary substitions * of parameter names. Also propagates non_null's.

  * * Precondition: rd has been typechecked.

### doSubst

    private static ExprModifierPragma doSubst(java.util.Hashtable subst,
                                              ExprModifierPragma emp)

  Perform a substitution on an ExprModifierPragma *

### doSubst

    private static CondExprModifierPragma doSubst(java.util.Hashtable subst,
                                                  CondExprModifierPragma emp)

  Perform a substitution on a CondExprModifierPragma *

### doSubst

    private static VarExprModifierPragma doSubst(java.util.Hashtable subst,
                                                 VarExprModifierPragma vemp)

  Perform a substitution on a VarExprModifierPragma *

### filterMethodDecl

    public static DerivedMethodDecl filterMethodDecl(DerivedMethodDecl dmd,
                                                     FindContributors scope)

### filterExprModPragmas

    private static ExprModifierPragmaVec filterExprModPragmas(ExprModifierPragmaVec vec,
                                                              FindContributors scope)

### filterModifies

    private static ModifiesGroupPragmaVec filterModifies(ModifiesGroupPragmaVec mvec,
                                                         FindContributors scope)

### filterVarExprModPragmas

    private static VarExprModifierPragmaVec filterVarExprModPragmas(VarExprModifierPragmaVec vec,
                                                                    FindContributors scope)

### trMethodDecl

    private static Spec trMethodDecl(DerivedMethodDecl dmd,
                                     java.util.Hashtable premap)

  Translates a MethodDecl to a Spec.

### trMethodDeclPreconditions

    private static ConditionVec trMethodDeclPreconditions(DerivedMethodDecl dmd,
                                                          ExprVec preAssumptions)

  Computes the preconditions, according to section 7.2.0 of ESCJ 16.

### trMethodDeclPostcondition

    private static ConditionVec trMethodDeclPostcondition(DerivedMethodDecl dmd,
                                                          java.util.Hashtable wt,
                                                          ExprVec postAssumptions)

  Computes the postconditions, according to section 7.2.2 of ESCJ 16.

### addAxioms

    public static void addAxioms(java.util.Set axsToAdd,
                                 ExprVec assumptions)

  axsToAdd holds a Set of RepHelper - we need to add to the assumptions any axioms pertinent to the RepHelper.

### addConstraintClauses

    public static ConditionVec addConstraintClauses(ConditionVec post,
                                                    TypeDecl decl,
                                                    java.util.Hashtable wt,
                                                    ExprVec postAssumptions)

### extendSpecForCall

    private static Spec extendSpecForCall(Spec spec,
                                          FindContributors scope,
                                          Set predictedSynTargs)

  Implements ExtendSpecForCall, section 7.3 of ESCJ 16.

### extendSpecForBody

    private static Spec extendSpecForBody(Spec spec,
                                          FindContributors scope,
                                          Set synTargs)

  Implements ExtendSpecForBody, section 7.4 of ESCJ 16.

### nonNullInitChecks

    private static void nonNullInitChecks(TypeDecl td,
                                          ConditionVec post)

  Add to `post` all NonNullInit checks for non_null instance fields and instance ghost fields declared in `td`.

### getFirstInheritedInterfaces

    public static java.util.Enumeration getFirstInheritedInterfaces(ClassDecl cd)

### addSuperInterfaces

    private static void addSuperInterfaces(TypeDecl td,
                                           Set set)

### addInvariantBody

    private static void 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`. The body to be checked has syntactic targets `synTargs`.

### collectAxioms

    private static ExprVec collectAxioms(FindContributors scope)

  Collects the axioms in `scope`.

### getRepresentsClauses

    public static TypeDeclElemVec getRepresentsClauses(TypeDecl td,
                                                       FieldDecl fd)

  Gets the represents clauses for a model field fd as seen from a type declaration td; fd may be declared in td or in a supertype of td. If td is null, then all represents clauses are returned, in any loaded class.

### collectInvariants

    private static InvariantInfo collectInvariants(FindContributors scope,
                                                   java.util.Hashtable premap)

### collectParamsAndGlobals

    private static ParamAndGlobalVarInfo collectParamsAndGlobals(Spec spec,
                                                                 FindContributors scope)

  Collects the parameters of `spec.args` and the static fields in `scope`, whose types are class types.

### addNewAxs

    private static ExprVec addNewAxs(java.util.HashSet axsToAdd,
                                     ExprVec assumptions)

### shave

    private static VariableAccess shave(Expr e)

  Shaves a GC designator.

### restrict

    static java.util.Hashtable restrict(java.util.Hashtable map,
                                        java.util.Enumeration e)

  Creates and returns a new map that is `map` restricted to the domain `e`. Assumes that every element in `e` is in the domain of `map`.

### makeSubst

    static java.util.Hashtable makeSubst(java.util.Enumeration e,
                                         java.lang.String postfix)

  Converts a GenericVarDecl enumeration to a mapping from those variables to new Variableaccesses.

### makeSubst

    static java.util.Hashtable makeSubst(FormalParaDeclVec args,
                                         java.lang.String postfix)

### createVarVariant

    static VariableAccess createVarVariant(GenericVarDecl vd,
                                           java.lang.String postfix)

  * Given a GenericVarDecl named "x@old", returns a VariableAccess to a * fresh LocalVarDecl named "x@ ". * * This handles ESCJ 23b case 13.

### addFreeTypeCorrectAs

    private static void addFreeTypeCorrectAs(GenericVarDecl vd,
                                             Type type,
                                             ConditionVec cv)

  Adds to `cv` a condition stating that `vd` has type `type`.

### surroundBodyBySpec

    public static GuardedCmd 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`.

### addAssumptions

    private static void addAssumptions(ExprVec ev,
                                       StackVector code)

  Appends `code` with an `assume C` command for every condition `C` in `cv`.

### assumeConditions

    private static void assumeConditions(ConditionVec cv,
                                         StackVector code)

### checkConditions

    private static void checkConditions(ConditionVec cv,
                                        int loc,
                                        StackVector code)

  Appends `code` with an `check loc: C` command for every condition `C` in `cv`.

### checkModifiesConstraints

    private static void checkModifiesConstraints(Spec spec,
                                                 FindContributors scope,
                                                 Set syntargets,
                                                 java.util.Hashtable premap,
                                                 int loc,
                                                 StackVector code)

### mergeInvariants

    private static InvariantInfo mergeInvariants(InvariantInfo ii)

### exprIsVisible

    private static boolean exprIsVisible(TypeSig originType,
                                         Expr e)

### collectFields

    public static void collectFields(Expr e,
                                     java.util.Set s)

### setNonNullPragma

    private static void setNonNullPragma(GenericVarDecl v,
                                         SimpleModifierPragma nonnull)

  * Mark v as non_null because of non_null pragma nonnull. * * Precondition: nonnull is a NON_NULL pragma. * * (Used to implement inheritence of non_null's.)

### NonNullPragma

    public static SimpleModifierPragma NonNullPragma(GenericVarDecl v)

  * Has a particular declaration been declared non_null? If so, * return the non_null pragma responsible. Otherwise, return null.

  * * Precondition: if the declaration is a formal parameter, then the * spec of it's routine has already been computed.

  * * * WARNING: this is the only authorized way to determine this * information. Do *not* attempt to search for NON_NULL modifiers * directly. (This is needed to handle inherited NON_NULL's * properly.)

### superNonNullPragma

    public static SimpleModifierPragma superNonNullPragma(GenericVarDecl v)

  Returns non-null if the formal parameter is declared non-null in some overridden declaration of the method.

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