de.uka.ilkd.key.rule.metaconstruct

Class WhileInvariantTransformer

java.lang.Object

de.uka.ilkd.key.rule.metaconstruct.WhileInvariantTransformer

public final class WhileInvariantTransformer
extends java.lang.Object

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
WhileInvariantTransformer()

Method Summary

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) Computes the TermLabel which should be added to the created loop body modality Term.
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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

outerLabel

private final SchemaVariable outerLabel

the outer label that is used to leave the while loop ('l1')

innerLabel

private final SchemaVariable innerLabel

the inner label ('l2')

instantiations

private ImmutableList<SchemaVariable> instantiations

list of the labels

breakList

private java.util.LinkedList<BreakToBeReplaced> breakList

list of breaks that lead to abrupt termination of the loop to be transformed. Is initialised by the method neededInstantiations that is invoked before calculate

javaInfo

private JavaInfo javaInfo

The JavaInfo object which is handed over as a parameter of calculate.

typeConv

private TypeConverter typeConv

tf

private TermFactory tf

body

private ProgramElement body

inv

private Term inv

post

private Term post

root

private JavaNonTerminalProgramElement root

modality

private Modality modality

returnType

private KeYJavaType returnType

Constructor Detail

WhileInvariantTransformer

public WhileInvariantTransformer()

Method Detail

init

private void init(Term initialPost,
                  Term invariantFramingTermination,
                  Services services)

initialises this meta operator

Parameters:

term - the instantiated Term passed to the TermTransformer

services - the Services providing access to signature and type model

transform

public 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.

computeLoopBodyModalityLabels

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)

Computes the TermLabel which should be added to the created loop body modality Term.

Parameters:

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.

Returns:

The TermLabels to add to the loop body modality Term.

getNewLocalvariable

private ProgramVariable getNewLocalvariable(java.lang.String varNameBase,
                                            java.lang.String varType,
                                            Services services)

creates a new program variable

Parameters:

varNameBase - a String specifying the basename of the new variable

varType - a String specifying the typename of the new variable

services - the Services allowing access to the variablenaming facilities

Returns:

a new program variable of the given type and a name as near as possible to the given basename

getNewLocalvariable

private ProgramVariable getNewLocalvariable(java.lang.String varNameBase,
                                            KeYJavaType varType,
                                            Services services)

creates a new program variable

Parameters:

varNameBase - a String specifying the basename of the new variable

varType - the KeYJavaType of the new variable

services - the Services allowing access to the variablenaming facilities

Returns:

a new program variable of the given type and a name as near as possible to the given basename

neededInstantiations

public ImmutableList<SchemaVariable> neededInstantiations(ProgramElement originalLoop,
                                                          SVInstantiations svInst)

returns the schemavariables that are needed to transform the given loop. The unwind-loop construct may need labels if unlabeled breaks and/or continues occur in the loop. Often there will be uninstantiated Schemavariables in the loop that is why the found instantiations have to be given.

createLongJunctorTerm

private Term createLongJunctorTerm(Junctor junctor,
                                   java.util.ArrayList<Term> terms)

returnFlagDecl

private Statement returnFlagDecl(ProgramVariable returnFlag,
                                 SVInstantiations svInst)

returnCase

private Term returnCase(TermLabelState termLabelState,
                        ProgramVariable returnFlag,
                        KeYJavaType returnType,
                        ProgramVariable returnExpression,
                        Term post,
                        Rule rule,
                        RuleApp ruleApp,
                        Goal goal,
                        PosInOccurrence applicationPos,
                        Services services)

breakFlagDecl

private Statement breakFlagDecl(ProgramVariable breakFlag)

contFlagDecl

private Statement contFlagDecl(ProgramVariable contFlag)

breakCase

private Term breakCase(TermLabelState termLabelState,
                       ProgramVariable breakFlag,
                       Term post,
                       java.util.ArrayList<If> breakIfCascade,
                       Rule rule,
                       RuleApp ruleApp,
                       Goal goal,
                       PosInOccurrence applicationPos,
                       Services services)

normalCaseAndContinue

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)

computeLoopBodyImplicatonLabels

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.

Parameters:

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.

Returns:

The TermLabels to add to the new Term.

throwCase

private Term throwCase(TermLabelState termLabelState,
                       ProgramVariable excFlag,
                       ProgramVariable thrownException,
                       Term post,
                       Rule rule,
                       RuleApp ruleApp,
                       Goal goal,
                       PosInOccurrence applicationPos,
                       Services services)

addContext

protected JavaBlock addContext(JavaNonTerminalProgramElement root,
                               StatementBlock block)