de.uka.ilkd.key.speclang

Class UnparameterizedMergeContract

java.lang.Object

de.uka.ilkd.key.speclang.UnparameterizedMergeContract

All Implemented Interfaces:

MergeContract, SpecificationElement

public class UnparameterizedMergeContract
extends java.lang.Object
implements MergeContract

A MergeContract for UnparametricMergeProcedures like MergeByIfThenElse.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private KeYJavaType	kjt
private MergeProcedure	mergeProcedure
private MergePointStatement	mps
private static java.lang.String	NAME

Constructor Summary

Constructors

Constructor and Description
UnparameterizedMergeContract(MergeProcedure mergeProcedure, MergePointStatement mps, KeYJavaType kjt)

Method Summary

Modifier and Type	Method and Description
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.
MergePointStatement	getMergePointStatement()
java.lang.Class<? extends MergeProcedure>	getMergeProcedure()
java.lang.String	getName() Returns the unique internal name of the specification element.

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

mergeProcedure

private final MergeProcedure mergeProcedure

mps

private final MergePointStatement mps

kjt

private final KeYJavaType kjt

Constructor Detail

UnparameterizedMergeContract

public UnparameterizedMergeContract(MergeProcedure mergeProcedure,
                                    MergePointStatement mps,
                                    KeYJavaType kjt)

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.

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