Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
AbstractionPredicate.create(Sort argSort,
java.util.function.Function<Term,Term> mapping,
Services services)
Creates a new
AbstractionPredicate with the given name and
mapping. |
static AbstractionPredicate |
AbstractionPredicate.create(Term predicate,
LocationVariable placeholder,
Services services)
Creates a new
AbstractionPredicate for the given predicate. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<AbstractionPredicate> |
AbstractionPredicate.fromString(java.lang.String s,
Services services,
NamespaceSet localNamespaces)
Parses the String representation of an abstraction predicates.
|
ImmutableSet<AbstractionPredicate> |
AbstractPredicateAbstractionDomainElement.getPredicates() |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> |
MergeWithPredicateAbstraction.getPredicates() |
Modifier and Type | Method and Description |
---|---|
void |
MergeWithPredicateAbstraction.addPredicate(AbstractionPredicate predicate)
Adds a new predicate to the set of abstraction predicates.
|
Modifier and Type | Method and Description |
---|---|
void |
MergeWithPredicateAbstraction.addPredicates(java.lang.Iterable<AbstractionPredicate> predicates)
Adds a new predicate to the set of abstraction predicates.
|
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.
|
void |
MergeWithPredicateAbstraction.setPredicates(java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> predicates) |
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.util.ArrayList<AbstractionPredicate> |
PredicateAbstractionMergeContract.getAbstractionPredicates(java.util.Map<LocationVariable,Term> atPres,
Services services)
TODO
|
Constructor and Description |
---|
PredicateAbstractionMergeContract(MergePointStatement mps,
java.util.Map<LocationVariable,Term> atPres,
KeYJavaType kjt,
java.lang.String latticeType,
java.util.List<AbstractionPredicate> abstractionPredicates) |
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
MergeRuleUtils.parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
Copyright © 2003-2019 The KeY-Project.