Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule.tacletbuilder | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Class and Description |
---|---|
class |
BlockInfFlowUnfoldTacletBuilder |
class |
InfFlowBlockContractTacletBuilder
Implements the rule which inserts operation contracts for a method call.
|
class |
InfFlowLoopInvariantTacletBuilder
Implements the rule which inserts loop invariants for a method call.
|
class |
InfFlowMethodContractTacletBuilder
Implements the rule which inserts operation contracts for a method call.
|
class |
LoopInfFlowUnfoldTacletBuilder |
class |
MethodInfFlowUnfoldTacletBuilder |
Modifier and Type | Method and Description |
---|---|
TermBuilder |
Services.getTermBuilder()
Returns the
TermBuilder used to create Term s. |
TermBuilder |
Services.getTermBuilder(boolean withCache)
Returns either the cache backed or raw
TermBuilder used to create Term s. |
Modifier and Type | Field and Description |
---|---|
protected TermBuilder |
ClashFreeSubst.tb |
Modifier and Type | Method and Description |
---|---|
TermBuilder |
TermServices.getTermBuilder()
Returns the
TermBuilder used to create Term s. |
TermBuilder |
TermServices.getTermBuilder(boolean withCache)
Returns either the cache backed or raw
TermBuilder used to create Term s. |
Constructor and Description |
---|
ClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
WaryClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
abstract Term |
SubstOp.apply(Term term,
TermBuilder tb)
Apply this substitution operator to
term , which
has this operator as top-level operator |
Term |
WarySubstOp.apply(Term term,
TermBuilder tb) |
Modifier and Type | Field and Description |
---|---|
protected TermBuilder |
AbstractPO.tb |
Constructor and Description |
---|
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
TermBuilder tb) |
Modifier and Type | Class and Description |
---|---|
static class |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder
This class is used to build various sub-formulas used in the block/loop contract rules.s
|
static class |
AuxiliaryContractBuilders.UpdatesBuilder
This class is used to build the various updates that are needed for block/loop contract
rules.
|
Modifier and Type | Field and Description |
---|---|
protected TermBuilder |
SyntacticalReplaceVisitor.tb
the termbuilder used to construct terms
|
Modifier and Type | Method and Description |
---|---|
protected static Term |
AbstractLoopInvariantRule.and(TermBuilder tb,
Term t1,
Term t2)
Creates a conjunction of t1 and t2 if both are not null, and returns t2
only if t1 is null.
|
protected static Term |
AbstractBlockContractRule.buildInfFlowPostAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPost,
Term baseHeap,
Term applPredTerm,
TermBuilder tb) |
protected static Term |
AbstractBlockContractRule.buildInfFlowPreAssumption(ProofObligationVars instVars,
ImmutableList<Term> localOuts,
ImmutableList<Term> localOutsAtPre,
Term baseHeap,
TermBuilder tb) |
protected void |
AbstractBlockContractRule.setUpInfFlowPartOfUsageGoal(Goal usageGoal,
AbstractBlockContractRule.InfFlowValidityData infFlowValitidyData,
Term contextUpdate,
Term remembranceUpdate,
Term anonymisationUpdate,
TermBuilder tb) |
Constructor and Description |
---|
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services,
TermBuilder termBuilder) |
Modifier and Type | Class and Description |
---|---|
protected static class |
AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract>
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
protected static class |
AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract>
This class contains a builder method for
AbstractAuxiliaryContractImpl s
(AbstractAuxiliaryContractImpl.Creator.create() ). |
static class |
AuxiliaryContract.VariablesCreator |
protected static class |
BlockContractImpl.Combinator
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
static class |
BlockContractImpl.Creator
This class is used to build
BlockContractImpl s. |
protected static class |
LoopContractImpl.Combinator
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
static class |
LoopContractImpl.Creator
This class is used to build
LoopContractImpl s. |
Modifier and Type | Method and Description |
---|---|
RepresentsAxiom |
RepresentsAxiom.conjoin(RepresentsAxiom ax,
TermBuilder tb)
Conjoins two represents clauses with minimum visibility.
|
Constructor and Description |
---|
Terms(AuxiliaryContract.Variables variables,
TermBuilder tb) |
Modifier and Type | Field and Description |
---|---|
protected TermBuilder |
JMLSpecFactory.tb |
Modifier and Type | Field and Description |
---|---|
TermBuilder |
JmlTermFactory.tb |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.translateToJDLTerm(org.antlr.runtime.Token escape,
java.lang.String functName,
Services services,
TermBuilder tb,
ImmutableList<SLExpression> list) |
Constructor and Description |
---|
SLResolverManager(SLExceptionFactory excManager,
KeYJavaType specInClass,
ParsableVariable selfVar,
boolean useLocalVarsAsImplicitReceivers,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
protected static Term |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
FormulaTermLabel label,
boolean antecedentRuleApplication,
TermBuilder tb)
Checks if new minor IDs are available.
|
protected static void |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available.
|
protected static Term |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
FormulaTermLabel label,
boolean antecedentRuleApplication,
TermBuilder tb)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
protected static void |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
protected static Term |
TruthValueTracingUtil.computeInstructionTerm(java.util.List<Term> antecedentReplacements,
java.util.List<Term> succedentReplacements,
boolean antecedentRuleApplication,
TermBuilder tb)
Computes the
Term with the instruction how to compute the truth
value based on the found replacements. |
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIds(Node childNode,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if available. |
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio,
PosInOccurrence parentPio,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if
available in case of OneStepSimplifier usage. |
Modifier and Type | Method and Description |
---|---|
protected Term |
ExecutionVariable.computeValueCondition(TermBuilder tb,
java.util.List<Goal> valueGoals,
InitConfig initConfig)
|
protected ExecutionValue[] |
ExecutionVariable.instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
Modifier and Type | Class and Description |
---|---|
class |
InfFlowProgVarRenamer |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
MiscTools.toTermList(java.lang.Iterable<ProgramVariable> list,
TermBuilder tb) |
Copyright © 2003-2019 The KeY-Project.