de.uka.ilkd.key.speclang

Interface MergeContract

All Superinterfaces:

SpecificationElement

All Known Implementing Classes:

PredicateAbstractionMergeContract, UnparameterizedMergeContract

public interface MergeContract
extends SpecificationElement

Specification of a MergePointStatement.

Author:

Dominic Scheurer

Method Summary

Modifier and Type	Method and Description
MergeProcedure	getInstantiatedMergeProcedure(Services services)
MergePointStatement	getMergePointStatement()
java.lang.Class<? extends MergeProcedure>	getMergeProcedure()
default VisibilityModifier	getVisibility() Returns the visibility of the invariant (null for default visibility)

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

getDisplayName, getKJT, getName

Method Detail

getMergePointStatement

MergePointStatement getMergePointStatement()

Returns:

The MergePointStatement specified by this MergeContract.

getMergeProcedure

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

Returns:

The MergeProcedure Class for the MergePointStatement.

getInstantiatedMergeProcedure

MergeProcedure getInstantiatedMergeProcedure(Services services)

Parameters:

services - TODO

Returns:

The instantiated MergeProcedure.

getVisibility

default VisibilityModifier getVisibility()

Description copied from interface: SpecificationElement

Returns the visibility of the invariant (null for default visibility)

Specified by:

getVisibility in interface SpecificationElement