public final class WhileInvariantTransformer
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ProgramElement |
body |
private java.util.LinkedList<BreakToBeReplaced> |
breakList
list of breaks that lead to abrupt termination of the loop to be
transformed.
|
private SchemaVariable |
innerLabel
the inner label ('l2')
|
private ImmutableList<SchemaVariable> |
instantiations
list of the labels
|
private Term |
inv |
private JavaInfo |
javaInfo
The JavaInfo object which is handed over as a parameter of calculate.
|
private Modality |
modality |
private SchemaVariable |
outerLabel
the outer label that is used to leave the while loop ('l1')
|
private Term |
post |
private KeYJavaType |
returnType |
private JavaNonTerminalProgramElement |
root |
private TermFactory |
tf |
private TypeConverter |
typeConv |
Constructor and Description |
---|
WhileInvariantTransformer() |
Modifier and Type | Method and Description |
---|---|
protected JavaBlock |
addContext(JavaNonTerminalProgramElement root,
StatementBlock block) |
private Term |
breakCase(TermLabelState termLabelState,
ProgramVariable breakFlag,
Term post,
java.util.ArrayList<If> breakIfCascade,
Rule rule,
RuleApp ruleApp,
Goal goal,
PosInOccurrence applicationPos,
Services services) |
private Statement |
breakFlagDecl(ProgramVariable breakFlag) |
private ImmutableArray<TermLabel> |
computeLoopBodyImplicatonLabels(TermLabelState termLabelState,
Services services,
PosInOccurrence applicationPos,
Rule rule,
RuleApp ruleApp,
Goal goal,
Operator operator,
ImmutableArray<Term> subs,
Sequent applicationSequent)
Computes the
TermLabel which should be added to the implication
of the normal termination branch of a loop body. |
private ImmutableArray<TermLabel> |
computeLoopBodyModalityLabels(TermLabelState termLabelState,
Services services,
PosInOccurrence applicationPos,
Rule rule,
RuleApp ruleApp,
Goal goal,
Operator loopBodyModality,
Term result,
JavaBlock mainJavaBlock,
Sequent applicationSequent,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
private Statement |
contFlagDecl(ProgramVariable contFlag) |
private Term |
createLongJunctorTerm(Junctor junctor,
java.util.ArrayList<Term> terms) |
private ProgramVariable |
getNewLocalvariable(java.lang.String varNameBase,
KeYJavaType varType,
Services services)
creates a new program variable
|
private ProgramVariable |
getNewLocalvariable(java.lang.String varNameBase,
java.lang.String varType,
Services services)
creates a new program variable
|
private void |
init(Term initialPost,
Term invariantFramingTermination,
Services services)
initialises this meta operator
|
ImmutableList<SchemaVariable> |
neededInstantiations(ProgramElement originalLoop,
SVInstantiations svInst)
returns the schemavariables that are needed to transform the given loop.
|
private Term |
normalCaseAndContinue(TermLabelState termLabelState,
Services services,
PosInOccurrence applicationPos,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
Term contFlagTerm,
Term returnFlagTerm,
Term breakFlagTerm,
Term excFlagTerm,
Term inv) |
private Term |
returnCase(TermLabelState termLabelState,
ProgramVariable returnFlag,
KeYJavaType returnType,
ProgramVariable returnExpression,
Term post,
Rule rule,
RuleApp ruleApp,
Goal goal,
PosInOccurrence applicationPos,
Services services) |
private Statement |
returnFlagDecl(ProgramVariable returnFlag,
SVInstantiations svInst) |
private Term |
throwCase(TermLabelState termLabelState,
ProgramVariable excFlag,
ProgramVariable thrownException,
Term post,
Rule rule,
RuleApp ruleApp,
Goal goal,
PosInOccurrence applicationPos,
Services services) |
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.
|
private final SchemaVariable outerLabel
private final SchemaVariable innerLabel
private ImmutableList<SchemaVariable> instantiations
private java.util.LinkedList<BreakToBeReplaced> breakList
private JavaInfo javaInfo
private TypeConverter typeConv
private TermFactory tf
private ProgramElement body
private Term inv
private Term post
private JavaNonTerminalProgramElement root
private Modality modality
private KeYJavaType returnType
private void init(Term initialPost, Term invariantFramingTermination, Services services)
term
- the instantiated Term passed to the TermTransformerservices
- the Services providing access to signature and type modelpublic Term transform(TermLabelState termLabelState, Rule rule, RuleApp ruleApp, Goal goal, Sequent applicationSequent, PosInOccurrence applicationPos, Term initialPost, Term invariantFramingTermination, SVInstantiations svInst, Services services)
private ImmutableArray<TermLabel> computeLoopBodyModalityLabels(TermLabelState termLabelState, Services services, PosInOccurrence applicationPos, Rule rule, RuleApp ruleApp, Goal goal, Operator loopBodyModality, Term result, JavaBlock mainJavaBlock, Sequent applicationSequent, ImmutableArray<TermLabel> newTermOriginalLabels)
termLabelState
- The TermLabelState
of the current rule application.services
- The Services
.applicationPos
- The PosInOccurrence
in the Sequent
to rewrite.rule
- The Rule
to apply.goal
- The Goal
to compute the result for.loopBodyModality
- The Modality
of the loop body.result
- The postcondition of the modality.mainJavaBlock
- The JavaBlock
to execute within the modality.applicationSequent
- The Sequent
to rewrite.TermLabel
s to add to the loop body modality
Term
.private ProgramVariable getNewLocalvariable(java.lang.String varNameBase, java.lang.String varType, Services services)
varNameBase
- a String specifying the basename of the new variablevarType
- a String specifying the typename of the new variableservices
- the Services allowing access to the variablenaming facilitiesprivate ProgramVariable getNewLocalvariable(java.lang.String varNameBase, KeYJavaType varType, Services services)
varNameBase
- a String specifying the basename of the new variablevarType
- the KeYJavaType of the new variableservices
- the Services allowing access to the variablenaming facilitiespublic ImmutableList<SchemaVariable> neededInstantiations(ProgramElement originalLoop, SVInstantiations svInst)
private Term createLongJunctorTerm(Junctor junctor, java.util.ArrayList<Term> terms)
private Statement returnFlagDecl(ProgramVariable returnFlag, SVInstantiations svInst)
private Term returnCase(TermLabelState termLabelState, ProgramVariable returnFlag, KeYJavaType returnType, ProgramVariable returnExpression, Term post, Rule rule, RuleApp ruleApp, Goal goal, PosInOccurrence applicationPos, Services services)
private Statement breakFlagDecl(ProgramVariable breakFlag)
private Statement contFlagDecl(ProgramVariable contFlag)
private Term breakCase(TermLabelState termLabelState, ProgramVariable breakFlag, Term post, java.util.ArrayList<If> breakIfCascade, Rule rule, RuleApp ruleApp, Goal goal, PosInOccurrence applicationPos, Services services)
private Term normalCaseAndContinue(TermLabelState termLabelState, Services services, PosInOccurrence applicationPos, Rule rule, RuleApp ruleApp, Goal goal, Sequent applicationSequent, Term contFlagTerm, Term returnFlagTerm, Term breakFlagTerm, Term excFlagTerm, Term inv)
private ImmutableArray<TermLabel> computeLoopBodyImplicatonLabels(TermLabelState termLabelState, Services services, PosInOccurrence applicationPos, Rule rule, RuleApp ruleApp, Goal goal, Operator operator, ImmutableArray<Term> subs, Sequent applicationSequent)
TermLabel
which should be added to the implication
of the normal termination branch of a loop body.termLabelState
- The TermLabelState
of the current rule application.services
- The Services
.applicationPos
- The PosInOccurrence
in the Sequent
to rewrite.rule
- The Rule
to apply.goal
- The Goal
to compute the result for.operator
- The Operator
of the new Term
.subs
- The children of the new Term
.applicationSequent
- The Sequent
to rewrite.TermLabel
s to add to the new Term
.private Term throwCase(TermLabelState termLabelState, ProgramVariable excFlag, ProgramVariable thrownException, Term post, Rule rule, RuleApp ruleApp, Goal goal, PosInOccurrence applicationPos, Services services)
protected JavaBlock addContext(JavaNonTerminalProgramElement root, StatementBlock block)