de.uka.ilkd.key.speclang

Class PredicateAbstractionMergeContract

java.lang.Object

de.uka.ilkd.key.speclang.PredicateAbstractionMergeContract

All Implemented Interfaces:

MergeContract, SpecificationElement

public class PredicateAbstractionMergeContract
extends java.lang.Object
implements MergeContract

A MergeContract for the MergeWithPredicateAbstraction MergeProcedure.

Author:

Dominic Scheurer

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
PredicateAbstractionMergeContract(MergePointStatement mps, java.util.Map<LocationVariable,Term> atPres, KeYJavaType kjt, java.lang.String latticeType, java.util.ArrayList<AbstractionPredicate> abstractionPredicates)

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.speclang.MergeContract

getVisibility

Field Detail

NAME

private static final java.lang.String NAME

See Also:

Constant Field Values

mps

private final MergePointStatement mps

atPres

private final java.util.Map<LocationVariable,Term> atPres

kjt

private final KeYJavaType kjt

latticeType

private final java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType

latticeTypeName

private final java.lang.String latticeTypeName

abstractionPredicates

private final java.util.ArrayList<AbstractionPredicate> abstractionPredicates

Constructor Detail

PredicateAbstractionMergeContract

public PredicateAbstractionMergeContract(MergePointStatement mps,
                                         java.util.Map<LocationVariable,Term> atPres,
                                         KeYJavaType kjt,
                                         java.lang.String latticeType,
                                         java.util.ArrayList<AbstractionPredicate> abstractionPredicates)

Method Detail

getMergeProcedure

public java.lang.Class<? extends MergeProcedure> getMergeProcedure()

Specified by:

getMergeProcedure in interface MergeContract

Returns:

The MergeProcedure Class for the MergePointStatement.

getInstantiatedMergeProcedure

public MergeProcedure getInstantiatedMergeProcedure(Services services)

Specified by:

getInstantiatedMergeProcedure in interface MergeContract

Parameters:

services - TODO

Returns:

The instantiated MergeProcedure.

getMergePointStatement

public MergePointStatement getMergePointStatement()

Specified by:

getMergePointStatement in interface MergeContract

Returns:

The MergePointStatement specified by this MergeContract.

getAtPres

public java.util.Map<LocationVariable,Term> getAtPres()

getLatticeType

public java.lang.Class<? extends AbstractPredicateAbstractionLattice> getLatticeType()

getLatticeTypeName

public java.lang.String getLatticeTypeName()

getAbstractionPredicates

public java.util.ArrayList<AbstractionPredicate> getAbstractionPredicates(java.util.Map<LocationVariable,Term> atPres,
                                                                          Services services)

TODO

Parameters:

atPres -

services -

Returns:

getName

public java.lang.String getName()

Description copied from interface: SpecificationElement

Returns the unique internal name of the specification element.

Specified by:

getName in interface SpecificationElement

getDisplayName

public java.lang.String getDisplayName()

Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement

getKJT

public KeYJavaType getKJT()

Description copied from interface: SpecificationElement

Returns the KeYJavaType representing the class/interface to which the specification element belongs.

Specified by:

getKJT in interface SpecificationElement

getReplaceMap

private java.util.Map<Term,Term> getReplaceMap(java.util.Map<LocationVariable,Term> atPres,
                                               Services services)

TODO

Parameters:

atPres -

services -

Returns:

latticeTypeFromString

private static java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeTypeFromString(java.lang.String latticeTypeStr)