public final class WhileInvariantTransformer
extends java.lang.Object
Constructor and Description |
---|
WhileInvariantTransformer() |
Modifier and Type | Method and Description |
---|---|
protected JavaBlock |
addContext(JavaNonTerminalProgramElement root,
StatementBlock block) |
ImmutableList<SchemaVariable> |
neededInstantiations(ProgramElement originalLoop,
SVInstantiations svInst)
returns the schemavariables that are needed to transform the given loop.
|
Term |
transform(TermLabelState termLabelState,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
PosInOccurrence applicationPos,
Term initialPost,
Term invariantFramingTermination,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
public Term transform(TermLabelState termLabelState, Rule rule, RuleApp ruleApp, Goal goal, Sequent applicationSequent, PosInOccurrence applicationPos, Term initialPost, Term invariantFramingTermination, SVInstantiations svInst, Services services)
public ImmutableList<SchemaVariable> neededInstantiations(ProgramElement originalLoop, SVInstantiations svInst)
protected JavaBlock addContext(JavaNonTerminalProgramElement root, StatementBlock block)
Copyright © 2003-2019 The KeY-Project.