Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of
Taclet s performing arithmetic operations. |
de.uka.ilkd.key.testgen |
Modifier and Type | Field and Description |
---|---|
protected SVInstantiations |
PrettyPrinter.instantiations |
Constructor and Description |
---|
PrettyPrinter(java.io.Writer o,
boolean noLinefeed,
SVInstantiations svi) |
PrettyPrinter(java.io.Writer o,
SVInstantiations svi) |
Constructor and Description |
---|
ProgramReplaceVisitor(ProgramElement root,
Services services,
SVInstantiations svi)
create the ProgramReplaceVisitor
|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars,
SVInstantiations svInst)
create the ProgramSVCollector
|
Modifier and Type | Method and Description |
---|---|
Term |
TermTransformer.transform(Term term,
SVInstantiations svInst,
Services services)
initiates term transformation of term.
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
LogicPrinter.getInstantiations() |
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printTaclet(Taclet taclet,
SVInstantiations sv,
boolean showWholeTaclet,
boolean declareSchemaVars)
Pretty-print a taclet.
|
void |
LogicPrinter.setInstantiation(SVInstantiations instantiations)
sets instantiations of schema variables
|
Constructor and Description |
---|
ProgramPrinter(java.io.Writer w,
boolean b,
SVInstantiations instantiations) |
ProgramPrinter(java.io.Writer writer,
SVInstantiations svi) |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
ProgVarReplacer.replace(SVInstantiations insts)
replaces in an SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
void |
Goal.addTaclet(Taclet rule,
SVInstantiations insts,
boolean isAxiom)
creates a new TacletApp and puts it to the set of TacletApps at the node
of the goal and to the current RuleAppIndex.
|
SVInstantiations |
ProgVarReplacer.replace(SVInstantiations insts)
replaces in an SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
OutputStreamProofSaver.getInteresting(SVInstantiations inst) |
Modifier and Type | Field and Description |
---|---|
protected SVInstantiations |
TacletApp.instantiations
contains the instantiations of the schema variables of the Taclet
|
protected SVInstantiations |
SyntacticalReplaceVisitor.svInst |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
MatchConditions.getInstantiations() |
SVInstantiations |
LightweightSyntacticalReplaceVisitor.getSVInstantiations() |
SVInstantiations |
SyntacticalReplaceVisitor.getSVInstantiations() |
SVInstantiations |
TacletApp.instantiations()
returns the instantiations for the application of the Taclet at the
specified position.
|
protected static SVInstantiations |
TacletApp.replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable varSV to a new LogicVariable.
|
protected static SVInstantiations |
TacletApp.resolveCollisionVarSV(Taclet taclet,
SVInstantiations insts,
Services services)
resolves collisions between bound SchemaVariables in an SVInstantiation
|
Modifier and Type | Method and Description |
---|---|
TacletApp |
NoPosTacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and hold the old ones
|
TacletApp |
PosTacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and the ones of this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations,
PosInOccurrence pos)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
abstract boolean |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
protected static boolean |
NoPosTacletApp.checkVarCondNotFreeIn(Taclet taclet,
SVInstantiations instantiations)
checks if the variable conditions of type 'x not free in y' are
hold by the found instantiations.
|
static boolean |
TacletApp.checkVarCondNotFreeIn(Taclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos)
checks if the variable conditions of type 'x not free in y' are hold by
the found instantiations.
|
static NoPosTacletApp |
NoPosTacletApp.createFixedNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
Create TacletApp with immutable "instantiations", i.e.
|
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
creates a NoPosTacletApp for the given taclet with some known
instantiations and CHECKS variable conditions as well as it
resolves collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
PosTacletApp.createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos,
Services services)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
protected static SVInstantiations |
TacletApp.replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable varSV to a new LogicVariable.
|
protected static SVInstantiations |
TacletApp.resolveCollisionVarSV(Taclet taclet,
SVInstantiations insts,
Services services)
resolves collisions between bound SchemaVariables in an SVInstantiation
|
protected TacletApp |
NoPosTacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the ones in this TacletApp
|
protected TacletApp |
PosTacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the old ones.
|
protected abstract TacletApp |
TacletApp.setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations and forget the old ones
|
MatchConditions |
MatchConditions.setInstantiations(SVInstantiations p_instantiations) |
Constructor and Description |
---|
LightweightSyntacticalReplaceVisitor(SVInstantiations svInst,
Services services)
constructs a term visitor replacing any occurrence of a schemavariable
found in
svInst by its instantiation |
MatchConditions(SVInstantiations p_instantiations,
RenameTable p_renameTable) |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
SVInstantiations svInst,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services)
constructs a term visitor replacing any occurrence of a schemavariable found
in
svInst by its instantiation |
TacletSchemaVariableCollector(SVInstantiations svInsts) |
Modifier and Type | Method and Description |
---|---|
boolean |
AlternativeVariableCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services)
check whether any of the two delegates apply
|
boolean |
ContainsAssignmentCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
boolean |
AbstractOrInterfaceType.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MayExpandMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
TypeComparisonCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayComponentTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
DifferentInstantiationCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
ArrayTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
IsThisReference.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
EnumTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
StaticFieldCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TermLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TypeCondition.check(SchemaVariable p_var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
LocalVariableCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
SubFormulaCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MetaDisjointCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
DifferentFields.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
ConstantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
FinalReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
FreeLabelInVariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
StaticMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
EnumConstantCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayLengthCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
StaticReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
abstract boolean |
TypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.GenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.NonGenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ElementTypeResolverForSV.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ContainerTypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
abstract Sort |
TypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.GenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.NonGenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ElementTypeResolverForSV.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ContainerTypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Modifier and Type | Field and Description |
---|---|
static SVInstantiations |
SVInstantiations.EMPTY_SVINSTANTIATIONS
the empty instantiation
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(GenericSortCondition p_c,
Services services)
Add the given additional condition for the generic sort instantiations
|
SVInstantiations |
SVInstantiations.add(ModalOperatorSV sv,
Operator op,
Services services) |
SVInstantiations |
SVInstantiations.add(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
adds the given pair to the instantiations for the context.If the context
has been instantiated already, the new pair is taken without a warning.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ImmutableArray<TermLabel> labels,
Services services) |
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramElement pe,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramList pes,
Services services) |
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
Term subst,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Name name,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
ProgramElement pe,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Term subst,
Services services) |
SVInstantiations |
SVInstantiations.addInterestingList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
SVInstantiations |
SVInstantiations.addList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
SVInstantiations |
SVInstantiations.addUpdate(Term update,
ImmutableArray<TermLabel> updateApplicationlabels)
adds an update to the update context
|
SVInstantiations |
SVInstantiations.addUpdateList(ImmutableList<SVInstantiations.UpdateLabelPair> updates) |
SVInstantiations |
SVInstantiations.clearUpdateContext() |
SVInstantiations |
SVInstantiations.makeInteresting(SchemaVariable sv,
Services services)
adds the schemvariable to the set of interesting ones
|
SVInstantiations |
SVInstantiations.replace(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ImmutableArray<ProgramElement> pes,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
Term term,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.union(SVInstantiations other,
Services services) |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.union(SVInstantiations other,
Services services) |
Modifier and Type | Field and Description |
---|---|
protected SVInstantiations |
WhileLoopTransformation.instantiations
if run in check mode there are normally schemavaribles, so we need the
instantiations of them
|
protected SVInstantiations |
ReplaceWhileLoop.instantiations
if run in check mode there are normally schemavaribles, so we need the
instantiations of them
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
ConstructorCall.constructorCallSequence(New constructorReference,
KeYJavaType classType,
SVInstantiations svInst,
Services services)
returns a sequence of statements modelling the Java constructor call
semantics explicitly
|
ImmutableList<SchemaVariable> |
WhileInvariantTransformer.neededInstantiations(ProgramElement originalLoop,
SVInstantiations svInst)
returns the schemavariables that are needed to transform the given loop.
|
ImmutableList<SchemaVariable> |
UnwindLoop.neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ImmutableList<SchemaVariable> |
ForToWhile.neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ImmutableList<SchemaVariable> |
ProgramTransformer.neededInstantiations(SVInstantiations svInst)
get a list of schema variables that are needed by this entity when
working given a SV instantiation set.
|
ProgramElement[] |
ReattachLoopInvariant.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
SpecialConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
UnwindLoop.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ForToWhile.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
StaticInitialisation.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
InitArrayCreation.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ArrayLength.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
IsStatic.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MultipleVarDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EvaluateArgs.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
TypeOf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
ArrayPostDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
DoBreak.transform(ProgramElement pe,
Services services,
SVInstantiations insts)
performs the program transformation needed for symbolic program
transformation
|
ProgramElement[] |
ConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MethodCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program execution
|
ProgramElement[] |
ForInitUnfoldTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EnhancedForElimination.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
An enhanced for loop is executed by transforming it into a "normal" for loop.
|
ProgramElement[] |
Unpack.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
PostWork.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program
transformation
|
abstract ProgramElement[] |
ProgramTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic
program transformation
|
ProgramElement[] |
SwitchToIf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
CreateObject.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ExpandMethodBody.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
Term |
WhileInvariantTransformer.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.
|
Term |
AddCast.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateBeforeLoopUpdate.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateLocalAnonUpdate.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
ConstantValue.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateFrameCond.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
ExpandQueriesMetaConstruct.transform(Term term,
SVInstantiations svInst,
Services services)
term.sub(0) is the term that possibly contains queries.
|
Term |
MemberPVToField.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
CreateWellformedCond.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
EnumConstantValue.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
ArrayBaseInstanceOf.transform(Term term,
SVInstantiations svInst,
Services services)
returns an G::instance(term.sub(1)) term for the element sort of
the given array .
|
Term |
CreateHeapAnonUpdate.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
IntroAtPreDefsOp.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
ObserverEqualityMetaConstruct.transform(Term term,
SVInstantiations svInst,
Services services)
Given two terms termExt and termBase, produce a formula which implies
equality of the two terms.
|
Constructor and Description |
---|
ReplaceWhileLoop(ProgramElement root,
SVInstantiations inst,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the check mode
|
WhileInvariantTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
WhileLoopTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
Modifier and Type | Method and Description |
---|---|
Term |
MetaGreater.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaEqual.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaArithBitMaskOp.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
DivideMonomials.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaLeq.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaSub.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
DivideLCRMonomials.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaShift.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaPow.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaDiv.transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Term |
MetaLess.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaGeq.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaAdd.transform(Term term,
SVInstantiations svInst,
Services services) |
Term |
MetaMul.transform(Term term,
SVInstantiations svInst,
Services services) |
Constructor and Description |
---|
CustomPrettyPrinter(java.io.Writer o,
boolean noLinefeed,
SVInstantiations svi) |
CustomPrettyPrinter(java.io.Writer o,
SVInstantiations svi) |
Copyright © 2003-2019 The KeY-Project.