public class StoreStmtInCondition extends java.lang.Object implements VariableCondition
Statement
, after substitution of
SchemaVariable
s, into the given ProgramSV
for later use in
other conditions and transformers. The arguments are a ProgramSV
and
a Term
, where the Term
must contain a JavaBlock
with
a StatementBlock
containing \modality{#allmodal}{ while (#e) #body }\endmodality(post)
);
this statement is then stored (in the example the while statement).Constructor and Description |
---|
StoreStmtInCondition(ProgramSV resultVarSV,
Term term) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
java.lang.String |
toString() |
public MatchConditions check(SchemaVariable sv, SVSubstitute instCandidate, MatchConditions matchCond, Services services)
VariableCondition
check
in interface VariableCondition
sv
- the SchemaVariable to be instantiatedinstCandidate
- the SVSubstitute (e.g. Term, ProgramElement) to be mapped to varmatchCond
- the MatchCondition with the current matching state and in particular
the SVInstantiations that are already known to be neededservices
- the program information objectnull
otherwisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.