public class PredicateAbstractionMergeContract extends java.lang.Object implements MergeContract
Modifier and Type | Field and Description |
---|---|
private java.util.ArrayList<AbstractionPredicate> |
abstractionPredicates |
private java.util.Map<LocationVariable,Term> |
atPres |
private KeYJavaType |
kjt |
private java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
latticeType |
private java.lang.String |
latticeTypeName |
private MergePointStatement |
mps |
private static java.lang.String |
NAME |
Constructor and Description |
---|
PredicateAbstractionMergeContract(MergePointStatement mps,
java.util.Map<LocationVariable,Term> atPres,
KeYJavaType kjt,
java.lang.String latticeType,
java.util.ArrayList<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.
|
private java.util.Map<Term,Term> |
getReplaceMap(java.util.Map<LocationVariable,Term> atPres,
Services services)
TODO
|
private static java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
latticeTypeFromString(java.lang.String latticeTypeStr) |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getVisibility
private static final java.lang.String NAME
private final MergePointStatement mps
private final java.util.Map<LocationVariable,Term> atPres
private final KeYJavaType kjt
private final java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType
private final java.lang.String latticeTypeName
private final java.util.ArrayList<AbstractionPredicate> abstractionPredicates
public PredicateAbstractionMergeContract(MergePointStatement mps, java.util.Map<LocationVariable,Term> atPres, KeYJavaType kjt, java.lang.String latticeType, java.util.ArrayList<AbstractionPredicate> abstractionPredicates)
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
private java.util.Map<Term,Term> getReplaceMap(java.util.Map<LocationVariable,Term> atPres, Services services)
atPres
- services
- private static java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeTypeFromString(java.lang.String latticeTypeStr)