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.backpred
Class BackPred

    java.lang.Object
      escjava.backpred.BackPred

public class BackPred
extends java.lang.Object

Generates the background predicate for a given type.

The background predicate for a particular class or interface type T consists of the conjunction of the background predicates contributions of each contributor class. See `FindContributors` for the definition of the contributors of a class.

A type must be typechecked in order to generate its background predicate. A type need only be prepped in order to generate its background predicate contribution.

Constructor Summary
`BackPred()`

Method Summary
`protected static void` | `addContribution(TypeDecl d, java.io.PrintStream proverStream)` Add to b the contribution from a particular TypeDecl, which is a formula.
`protected static void` | `bg(java.lang.String s, java.io.PrintStream proverStream)` Called with a simplify command.
`protected static void` | `bgi(java.lang.String s, java.io.PrintStream proverStream)` Called with an S-expression that may contain a free variable "t".
`protected static Expr` | `eq(Expr e1, Expr e2, Type t)` Generate the appropriate GC equality e1 == e2 based on type t.
`protected static LiteralExpr` | `eval(Expr e, int loc)` Like ConstantExpr.eval, but returns a LiteralExpr instead of an Integer/Long/etc.
`private static void` | `genFinalInitInfo(VarInit initExpr, GenericVarDecl sDecl, Expr s, Expr x, Type type, int loc, java.io.PrintStream proverStream)`
`static void` | `genTypeBackPred(FindContributors scope, java.io.PrintStream proverStream)` Return the type-specific background predicate as a formula.
`static void` | `genUnivBackPred(java.io.PrintStream proverStream)` Returns the universal background predicate as a sequence of simplify commands.
`protected static boolean` | `isStaticallyNonNull(VarInit e)` Do we know statically that an expression always returns a non-null value?
`private static void` | `produce(GenericVarDecl sDecl, Expr s, Expr e, java.io.PrintStream proverStream)`
`private static void` | `sayIsFinal(Type x, java.io.PrintStream proverStream)` Record in the background predicate that x is final.
`private static void` | `saySubClass(Type x, Type y, java.io.PrintStream proverStream)` Record in the background predicate that x is a subclass of y.
`private static void` | `saySubType(Type x, Type y, java.io.PrintStream proverStream)` Record in the background predicate that x is a subtype of y.
`private static void` | `saySuper(TypeDecl d, java.io.PrintStream proverStream)`
`static java.lang.String` | `simplifyTypeName(Type x)`

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

Constructor Detail

### BackPred

    public BackPred()

Method Detail

### genUnivBackPred

    public static void genUnivBackPred(java.io.PrintStream proverStream)

  Returns the universal background predicate as a sequence of simplify commands.

### genTypeBackPred

    public static void genTypeBackPred(FindContributors scope,
                                       java.io.PrintStream proverStream)

  Return the type-specific background predicate as a formula.

### genFinalInitInfo

    private static void genFinalInitInfo(VarInit initExpr,
                                         GenericVarDecl sDecl,
                                         Expr s,
                                         Expr x,
                                         Type type,
                                         int loc,
                                         java.io.PrintStream proverStream)

### produce

    private static void produce(GenericVarDecl sDecl,
                                Expr s,
                                Expr e,
                                java.io.PrintStream proverStream)

### addContribution

    protected static void addContribution(TypeDecl d,
                                          java.io.PrintStream proverStream)

  Add to b the contribution from a particular TypeDecl, which is a formula.

### saySubClass

    private static void saySubClass(Type x,
                                    Type y,
                                    java.io.PrintStream proverStream)

  Record in the background predicate that x is a subclass of y.

### saySubType

    private static void saySubType(Type x,
                                   Type y,
                                   java.io.PrintStream proverStream)

  Record in the background predicate that x is a subtype of y.

### saySuper

    private static void saySuper(TypeDecl d,
                                 java.io.PrintStream proverStream)

### sayIsFinal

    private static void sayIsFinal(Type x,
                                   java.io.PrintStream proverStream)

  Record in the background predicate that x is final.

### simplifyTypeName

    public static java.lang.String simplifyTypeName(Type x)

### bgi

    protected static void bgi(java.lang.String s,
                              java.io.PrintStream proverStream)

  Called with an S-expression that may contain a free variable "t". Wraps "(FORALL (s) (IMPLIES (NEQ s null) " and "))" around this expression and adds it to the background predicate.

### bg

    protected static void bg(java.lang.String s,
                             java.io.PrintStream proverStream)

  Called with a simplify command. Adds it to the background predicate.

### isStaticallyNonNull

    protected static boolean isStaticallyNonNull(VarInit e)

  Do we know statically that an expression always returns a non-null value?

### eval

    protected static LiteralExpr eval(Expr e,
                                      int loc)

  Like ConstantExpr.eval, but returns a LiteralExpr instead of an Integer/Long/etc.

  Ignores String constants. (Always returns null in that case.)

  If returns a non-null LiteralExpr, sets its loc to `loc`.

### eq

    protected static Expr eq(Expr e1,
                             Expr e2,
                             Type t)

  Generate the appropriate GC equality e1 == e2 based on type t.

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