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

escjava.backpred
Class BackPred

java.lang.Object
  extended byescjava.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.


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

The ESC/Java2 Project Homepage