public static final class AbstractAuxiliaryContractRule.Instantiation
extends java.lang.Object
AbstractAuxiliaryContractBuiltInRuleApp
Modifier and Type | Field and Description |
---|---|
ExecutionContext |
context
The execution context in which the block occurs.
|
Term |
formula
The update target.
|
Modality |
modality
The contract's modality.
|
Term |
self
The self variable.
|
JavaStatement |
statement
The statement the contract belongs to.
|
Term |
update
The context update.
|
Constructor and Description |
---|
Instantiation(Term update,
Term formula,
Modality modality,
Term self,
JavaStatement statement,
ExecutionContext context) |
Modifier and Type | Method and Description |
---|---|
boolean |
isTransactional() |
public final Term update
public final Term formula
public final Modality modality
public final Term self
public final JavaStatement statement
public final ExecutionContext context
public Instantiation(Term update, Term formula, Modality modality, Term self, JavaStatement statement, ExecutionContext context)
update
- the context update.formula
- the update target.modality
- the modality.self
- the self variable.statement
- the statement the contract belongs to.context
- the execution context in which the block occurs.