public interface MergeContract extends SpecificationElement
MergePointStatement
.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)
|
MergeContract |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
getDisplayName, getKJT, getName
MergeContract map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface SpecificationElement
op
- the operator to apply.services
- services.MergePointStatement getMergePointStatement()
MergePointStatement
specified by this MergeContract
.java.lang.Class<? extends MergeProcedure> getMergeProcedure()
MergeProcedure
Class
for the MergePointStatement
.MergeProcedure getInstantiatedMergeProcedure(Services services)
services
- TODOMergeProcedure
.default VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
Copyright © 2003-2019 The KeY-Project.