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.ast
Class AnOverview

    java.lang.Object
      javafe.ast.ASTNode
          escjava.ast.AnOverview

All Implemented Interfaces:
  java.lang.Cloneable

public abstract class AnOverview
extends ASTNode

The files in this package extend the AST classes defined in `javafe.ast`. The following diagram shows how the new classes related to the old classes in the class hierarchy:

     - ASTNode
        - VarInit ()
           - Expr ()
             + GCExpr
               + LabelExpr (Identifier label, Expr expr)
               + NaryExpr (int op, Identifier methodName, Expr* exprs)
               + QuantifiedExpr (GenericVarDecl* vars, Expr rangeExpr, Expr expr)
               + GeneralizedQuantifiedExpr (GenericVarDecl* vars, Expr expr)
                    // Sum, Product, Max, Min
               + NumericalQuantifiedExpr (GenericVarDecl* vars, Expr expr)
                    // NumOf
               + SubstExpr (GenericVarDecl var, Expr val, Expr target)
               + TypeExpr (Type type)
             + EverythingExpr ()
             + LockSetExpr ()
             + NotSpecifiedExpr ()
             + NothingExpr ()
             + StoreRefExpr(Expr,Expr)
             + NotModifiedExpr(Expr)
             + ResExpr ()
    	   + SetCompExpr(Type type, Type typeBound, Identifier id, Expr e)
             + WildRefExpr (Expr expr)
             + GuardExpr (Expr expr)
             + DefPredLetExpr (DefPred* preds, Expr body)
             + DefPredApplExpr (Identifier predId, Expr* args)
    	   + ArrayRangeRefExpr(Expr, Expr, Expr)
        + GuardedCmd
          + SimpleCmd (int cmd) // Skip, Raise
          + ExprCmd (int cmd, Expr pred) // Assert, Assume
          + AssignCmd (VariableAccess v, Expr rhs)
            + GetsCmd ()
            + SubGetsCmd (Expr index)
            + SubSubGetsCmd (Expr index1, Expr index2)
            + RestoreFromCmd ()
          + VarInCmd (GenericVarDecl v*, GuardedCmd g)
          + DynInstCmd (String s, GuardedCmd g)
          + SeqCmd (GuardedCmd cmds*)
          + LoopCmd (Condition invariants*, DecreasesInfo decreases*,
                     LocalVarDecl skolemConstants*, Expr predicates*,
                     GenericVarDecl tempVars*, GuardedCmd guard, GuardedCmd body)
          + CmdCmdCmd (int cmd, GuardedCmd g1, GuardedCmd g2)// Try, Choose
          + Call (RoutineDecl rd, Expr* args, TypeDecl scope)
        - TypeDeclElem ()
           - TypeDeclElemPragma ()
             + ExprDeclPragma (Expr expr) // Axiom, ObjectInvariant
    	   + GhostDeclPragma (GhostFieldDecl decl)
    	   + ModelDeclPragma (ModelFieldDecl decl)
             + ModelTypePragma (TypeDecl decl)
             + NamedExprDeclPragma (Expr target, Expr expr)
             + IdExprDeclPragma (Id target, Expr expr)
             + ModelMethodDeclPragma (MethodDecl decl)
             + ModelConstructorPragma (ConstructorDecl decl)
             + StillDeferredDeclPragma (Identifier var)
             + DependsPragma (Expr* exprs) // Depends clause
        - Stmt ()
           - StmtPragma ()
             + SimpleStmtPragma () // Unreachable
             + ExprStmtPragma (Expr expr, Expr label)
                 // Assume, Assert, LoopInvariant, LoopPredicate
             + SetStmtPragma (Expr target, Expr value)
             + SkolemConstantPragma (LocalVarDecl* decl)
        - ModifierPragma ()
             + SimpleModifierPragma ()
                       // Uninitialized, Monitored, NonNull, WritableDeferred,
                       // Helper, \Peer, \ReadOnly, \Rep,
                       // may_be_null, null_ref_by_default, non_null_ref_by_default,
                       // obs_pure,
                       // code_java_math, code_safe_math, code_bigint_math,
                       // spec_java_math, spec_safe_math, spec_bigint_math
    	   + NestedModifierPragma (ArrayList list)
             + ExprModifierPragma (Expr expr)
                       // DefinedIf, Writable, Requires, Pre, Ensures, Post,
                       // AlsoEnsures, MonitoredBy, Constraint, InvariantFor, Space,
                       // \Duration, \WorkingSpace,
                       // \java_math, \safe_math, \bigint_math
             + IdentifierModifierPramga (Identifier id)
                       // IsInitialized
             + ReachModifierPragma (Expr expr, Identifier id, StoreRefExpr)
                       // \Reach
    	   + CondExprModifierPragma (Expr expr, Expr cond)
                       // Modifies, AlsoModifiers, Assignable, Modifiable
             + ModifiesGroupPragma
                       // Group of Modifies, etc., pragmas from one spec case
             + MapsExprModifierPragma (Identifier id, Expr mapsexpr, Expr expr)
    		     // maps
             + VarExprModifierPragma (GenericVarDecl arg, Expr expr)
                       // Exsures, AlsoExsures, Signals, AlsoSignals
             + ModelProgramModifierPragma()
    	   + VarDeclModifierPragma (LocalVarDecl decl)
        - LexicalPragma ()
          + NowarnPragma (Identifier* checks)
          + ImportPragma (ImportDecl decl)
          + RefinePragma (String filename)
        + Spec (MethodDecl md, Expr* targets, Hashtable preVarMap,
                Condition* pre, Condition* post)
        + Condition(int label, Expr pred)
        + DefPred (Identifier predId, GenericVarDecl* args, Expr body)

(Classes with a `-` next to them are defined in `javafe.ast`; classes with a `+` are defined in this package.

(P.S. Ignore the stuff that appears below; the only purpose of this class is to contain the above overview.)

Field Summary

Fields inherited from class javafe.ast.ASTNode
``

Constructor Summary
`AnOverview()`

Method Summary
`abstract void` | `accept(Visitor v)` Accept a visit from `v`.
`abstract java.lang.Object` | `accept(VisitorArgResult v, java.lang.Object o)`
`void` | `check()`
`abstract java.lang.Object` | `childAt(int i)` Return the first-but-ith child of a node.
`abstract int` | `childCount()` Return the number of children a node has.
`abstract int` | `getTag()` Return the tag of a node.
`abstract java.lang.String` | `toString()` Return a string representation of `this`.

Methods inherited from class javafe.ast.ASTNode
`clone, clone, getDecorations, getEndLoc, getStartLoc, setDecorations`

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

Constructor Detail

### AnOverview

    public AnOverview()

Method Detail

### childCount

    public abstract int childCount()

  Return the number of children a node has.

  Specified by:
    `childCount` in class `ASTNode`

### childAt

    public abstract java.lang.Object childAt(int i)

  Return the first-but-ith child of a node.

  Specified by:
    `childAt` in class `ASTNode`

### getTag

    public abstract int getTag()

  Return the tag of a node.

  Specified by:
    `getTag` in class `ASTNode`

### toString

    public abstract java.lang.String toString()

  Return a string representation of `this`. Meant for debugging use only, not for presentation.

  Specified by:
    `toString` in class `ASTNode`

### accept

    public abstract void accept(Visitor v)

  Accept a visit from `v`. This method simply calls the method of `v` corresponding to the allocated type of `this`, passing `this` as the argument. See the design patterns book.

  Specified by:
    `accept` in class `ASTNode`

### accept

    public abstract java.lang.Object accept(VisitorArgResult v,
                                            java.lang.Object o)

  Specified by:
    `accept` in class `ASTNode`

### check

    public void check()

  Overrides:
    `check` in class `ASTNode`

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