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.pa
Class PredicateAbstraction

    java.lang.Object
      escjava.pa.PredicateAbstraction

public class PredicateAbstraction
extends java.lang.Object

Field Summary
`Abstractor` | `abstractor`
`private mocha.wrappers.jbdd.jbddManager` | `bddManager`
`private GuardedCmd` | `body`
`private GuardedCmd` | `bodyDesugared`
`private StackVector` | `code`
`private GuardedCmd` | `havoc`
`(package private) ExprVec` | `invariants`
`private ExprVec` | `loopPredicates`
`(package private) long` | `milliSecsUsed`
`int` | `nQueries`
`static ASTDecoration` | `paDecoration`
`(package private) GCProver` | `perfCount`
`private static boolean` | `quantifyAssumptions`
`private LocalVarDeclVec` | `skolemConstants`
`private int` | `startLoc`
`private GenericVarDeclVec` | `temporaries`

Constructor Summary
`(package private)` | `PredicateAbstraction(LoopCmd g, Set env)`

Method Summary
`(package private) static GuardedCmd` | `abstractLoop(LoopCmd g, GuardedCmd context, Set env)`
`private GuardedCmd` | `abstractLoopHelper(GuardedCmd context, Set env)`
`private void` | `guessPredicate(Expr e, Expr eOld, Type type, ExprVec predicates, int loc, Expr sca, ExprVec boundsSC)`
`private void` | `inferPredicates(LoopCmd g, Set env, Set targets)`
`private static boolean` | `mentions(Expr e, GenericVarDecl d)`
`static ExprVec` | `skolemQuantInvariants(LocalVarDeclVec skolemConstants, ExprVec invs, int sloc, int eloc)`

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

Field Detail

### paDecoration

    public static ASTDecoration paDecoration

### quantifyAssumptions

    private static boolean quantifyAssumptions

### invariants

    ExprVec invariants

### bddManager

    private mocha.wrappers.jbdd.jbddManager bddManager

### abstractor

    public Abstractor abstractor

### skolemConstants

    private LocalVarDeclVec skolemConstants

### loopPredicates

    private ExprVec loopPredicates

### body

    private GuardedCmd body

### bodyDesugared

    private GuardedCmd bodyDesugared

### havoc

    private GuardedCmd havoc

### startLoc

    private int startLoc

### nQueries

    public int nQueries

### milliSecsUsed

    long milliSecsUsed

### perfCount

    GCProver perfCount

### code

    private final StackVector code

### temporaries

    private final GenericVarDeclVec temporaries

Constructor Detail

### PredicateAbstraction

    PredicateAbstraction(LoopCmd g,
                         Set env)

Method Detail

### abstractLoop

    static GuardedCmd abstractLoop(LoopCmd g,
                                   GuardedCmd context,
                                   Set env)

### abstractLoopHelper

    private GuardedCmd abstractLoopHelper(GuardedCmd context,
                                          Set env)

### skolemQuantInvariants

    public static ExprVec skolemQuantInvariants(LocalVarDeclVec skolemConstants,
                                                ExprVec invs,
                                                int sloc,
                                                int eloc)

### mentions

    private static boolean mentions(Expr e,
                                    GenericVarDecl d)

### inferPredicates

    private void inferPredicates(LoopCmd g,
                                 Set env,
                                 Set targets)

### guessPredicate

    private void guessPredicate(Expr e,
                                Expr eOld,
                                Type type,
                                ExprVec predicates,
                                int loc,
                                Expr sca,
                                ExprVec boundsSC)

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