Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.proof.io.intermediate | |
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
ConjunctivePredicateAbstractionLattice
A lattice for all predicates accepting the given sort.
|
class |
DisjunctivePredicateAbstractionLattice
A lattice for all predicates accepting the given sort.
|
class |
SimplePredicateAbstractionLattice
A lattice for all predicates accepting the given sort.
|
Modifier and Type | Method and Description |
---|---|
java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
MergeAppIntermediate.getPredAbstrLatticeType() |
Constructor and Description |
---|
MergeAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int id,
java.lang.String joinProc,
int nrPartners,
ImmutableList<Name> newNames,
java.lang.String distinguishingFormula,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType,
java.lang.String abstractionPredicates,
java.lang.String userChoices)
Constructs a new join rule.
|
Modifier and Type | Method and Description |
---|---|
java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
MergeWithPredicateAbstraction.getLatticeType() |
Modifier and Type | Method and Description |
---|---|
MergeWithPredicateAbstraction |
MergeWithPredicateAbstractionFactory.instantiate(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices)
Creates a complete instance of
MergeWithPredicateAbstraction . |
static AbstractDomainLattice |
MergeWithPredicateAbstraction.instantiateAbstractDomain(Sort s,
java.util.List<AbstractionPredicate> applicablePredicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
Services services)
Instantiates the abstract domain lattice for the given sort or null if
there has no lattice been specified for that sort.
|
Constructor and Description |
---|
MergeWithPredicateAbstraction(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.Map<ProgramVariable,AbstractDomainElement> userChoices)
Creates a new instance of
MergeWithPredicateAbstraction . |
Modifier and Type | Method and Description |
---|---|
java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
PredicateAbstractionMergeContract.getLatticeType() |
Copyright © 2003-2019 The KeY-Project.