public static final class UseOperationContractRule.Instantiation
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
ImmutableList<Term> |
actualParams
The actual parameter terms.
|
Expression |
actualResult
The actual result expression.
|
Term |
actualSelf
The actual self term.
|
Modality |
mod
The modality.
|
MethodOrConstructorReference |
mr
TODO
|
IProgramMethod |
pm
The program method.
|
Term |
progPost
The program post condition term.
|
KeYJavaType |
staticType
The static KeYJavaType.
|
boolean |
transaction
TODO
|
Term |
u
The enclosing update term.
|
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
Modality mod,
Expression actualResult,
Term actualSelf,
KeYJavaType staticType,
MethodOrConstructorReference mr,
IProgramMethod pm,
ImmutableList<Term> actualParams,
boolean transaction)
Creates a new instantiation for the contract rule and the given variables.
|
public final Term u
public final Term progPost
public final Modality mod
public final Expression actualResult
public final Term actualSelf
public final KeYJavaType staticType
public final MethodOrConstructorReference mr
public final IProgramMethod pm
public final ImmutableList<Term> actualParams
public final boolean transaction
public Instantiation(Term u, Term progPost, Modality mod, Expression actualResult, Term actualSelf, KeYJavaType staticType, MethodOrConstructorReference mr, IProgramMethod pm, ImmutableList<Term> actualParams, boolean transaction)
u
- the enclosing update termprogPost
- the post condition of the program methodmod
- the modalityactualResult
- the result expressionactualSelf
- the self termstaticType
- the static typemr
- TODOpm
- the program methodactualParams
- the actual parameter termstransaction
- TODOCopyright © 2003-2019 The KeY-Project.