public class PredicateAbstractionMergeContract extends java.lang.Object implements MergeContract
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 |
---|---|
java.util.ArrayList<AbstractionPredicate> |
getAbstractionPredicates(java.util.Map<LocationVariable,Term> atPres,
Services services)
TODO
|
java.util.Map<LocationVariable,Term> |
getAtPres() |
java.lang.String |
getDisplayName()
Returns the displayed name.
|
MergeProcedure |
getInstantiatedMergeProcedure(Services services) |
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
getLatticeType() |
java.lang.String |
getLatticeTypeName() |
MergePointStatement |
getMergePointStatement() |
java.lang.Class<? extends MergeProcedure> |
getMergeProcedure() |
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
PredicateAbstractionMergeContract |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getVisibility
public PredicateAbstractionMergeContract(MergePointStatement mps, java.util.Map<LocationVariable,Term> atPres, KeYJavaType kjt, java.lang.String latticeType, java.util.List<AbstractionPredicate> abstractionPredicates)
public PredicateAbstractionMergeContract map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface MergeContract
map
in interface SpecificationElement
op
- the operator to apply.services
- services.public java.lang.Class<? extends MergeProcedure> getMergeProcedure()
getMergeProcedure
in interface MergeContract
MergeProcedure
Class
for the MergePointStatement
.public MergeProcedure getInstantiatedMergeProcedure(Services services)
getInstantiatedMergeProcedure
in interface MergeContract
services
- TODOMergeProcedure
.public MergePointStatement getMergePointStatement()
getMergePointStatement
in interface MergeContract
MergePointStatement
specified by this MergeContract
.public java.util.Map<LocationVariable,Term> getAtPres()
public java.lang.Class<? extends AbstractPredicateAbstractionLattice> getLatticeType()
public java.lang.String getLatticeTypeName()
public java.util.ArrayList<AbstractionPredicate> getAbstractionPredicates(java.util.Map<LocationVariable,Term> atPres, Services services)
atPres
- services
- public java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
Copyright © 2003-2019 The KeY-Project.