Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.mergerule | |
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
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.nparser.builder | |
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.proof.io.intermediate | |
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Pair<LocationVariable,Term> |
AbstractionPredicate.getPredicateFormWithPlaceholder() |
Modifier and Type | Method and Description |
---|---|
Pair<java.lang.String,Location> |
KeYEnvironment.getProofScript() |
Constructor and Description |
---|
KeYEnvironment(U ui,
InitConfig initConfig,
Proof loadedProof,
Pair<java.lang.String,Location> proofScript,
AbstractProblemLoader.ReplayResult replayResult)
Constructor
|
Modifier and Type | Method and Description |
---|---|
protected static Pair<java.io.File,java.lang.String> |
WindowUserInterfaceControl.fileName(Proof proof,
java.lang.String fileExtension) |
Constructor and Description |
---|
ClassTree(boolean addContractTargets,
boolean skipLibraryClasses,
Services services,
java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons) |
Modifier and Type | Method and Description |
---|---|
abstract C |
MergeProcedureCompletion.complete(C proc,
Pair<Goal,PosInOccurrence> mergeGoalPio,
java.util.Collection<MergePartner> partners)
Completes the given merge procedure either automatically (if the procedure
is already complete) or by demanding input from the user in a GUI.
|
Modifier and Type | Method and Description |
---|---|
MergeWithPredicateAbstraction |
PredicateAbstractionCompletion.complete(MergeWithPredicateAbstraction proc,
Pair<Goal,PosInOccurrence> joinGoalPio,
java.util.Collection<MergePartner> partners) |
Modifier and Type | Method and Description |
---|---|
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeConstantLabels(Model model) |
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeFields(ObjectVal ov) |
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeFunctions(ObjectVal ov) |
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeObjectProperties(ObjectVal ov,
java.lang.String sortName) |
Modifier and Type | Method and Description |
---|---|
LRUCache<Pair<Term,Term>,Term> |
ServiceCaches.getProvedByArithSndCache() |
Modifier and Type | Method and Description |
---|---|
static Pair<ImmutableList<Term>,Term> |
TermBuilder.goBelowUpdates2(Term term)
Removes leading updates from the passed term.
|
Modifier and Type | Method and Description |
---|---|
Sort |
DefaultBuilder.toArraySort(Pair<Sort,Type> p,
int numOfDimensions) |
Modifier and Type | Method and Description |
---|---|
java.util.List<Pair<java.lang.String,java.lang.String>> |
Statistics.getSummary() |
Modifier and Type | Method and Description |
---|---|
Pair<java.lang.String,Location> |
AbstractProblemLoader.getProofScript() |
Pair<java.lang.String,Location> |
AbstractProblemLoader.readProofScript() |
Modifier and Type | Method and Description |
---|---|
Pair<java.lang.Integer,PosInTerm> |
BuiltInAppIntermediate.getPosInfo() |
Pair<java.lang.Integer,PosInTerm> |
TacletAppIntermediate.getPosInfo() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Pair<java.lang.Integer,PosInTerm>> |
BuiltInAppIntermediate.getBuiltInIfInsts() |
Constructor and Description |
---|
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
MergeAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int id,
java.lang.String joinProc,
int nrPartners,
ImmutableList<Name> newNames,
java.lang.String distinguishingFormula,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType,
java.lang.String abstractionPredicates,
java.lang.String userChoices)
Constructs a new join rule.
|
MergePartnerAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int mergeNodeId,
ImmutableList<Name> newNames)
Constructs a new close-merge-partner intermediate application.
|
TacletAppIntermediate(java.lang.String tacletName,
Pair<java.lang.Integer,PosInTerm> posInfo,
java.util.LinkedList<java.lang.String> insts,
ImmutableList<java.lang.String> ifSeqFormulaList,
ImmutableList<java.lang.String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
Constructor and Description |
---|
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
Modifier and Type | Method and Description |
---|---|
Pair<IObserverFunction,ImmutableSet<Taclet>> |
SpecificationRepository.limitObs(IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
SpecificationRepository.getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
Modifier and Type | Method and Description |
---|---|
protected static Pair<Term,Term> |
AbstractLoopInvariantRule.prepareVariant(AbstractLoopInvariantRule.Instantiation inst,
Term variant,
TermServices services)
Creates the variant proof obligation and update.
|
Pair<Term,Term> |
QueryExpand.queryEvalTerm(Services services,
Term query,
LogicVariable[] instVars)
Creates an invocation of a query in a modal operator and stores the value in a
new symbol.
|
protected static Pair<Term,Term> |
AbstractLoopInvariantRule.splitUpdates(Term focusTerm,
TermServices services)
Splits a term into the update and formula part.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Modifier and Type | Method and Description |
---|---|
abstract ImmutableSet<Pair<Sort,IObserverFunction>> |
ClassAxiom.getUsedObservers(Services services)
Returns the pairs (kjt, obs) for which there is an occurrence of
o.obs in the axiom, where kjt is the type of o (excluding the
defining occurrence of the axiom target).
|
ImmutableSet<Pair<Sort,IObserverFunction>> |
ClassAxiomImpl.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
QueryAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
PartialInvAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
ContractAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
RepresentsAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
ModelMethodExecution.getUsedObservers(Services services) |
Modifier and Type | Method and Description |
---|---|
abstract ImmutableSet<Taclet> |
ClassAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services)
The axiom as one or many taclets, where the non-defining occurrences of
the passed observers are replaced by their "limited" counterparts.
|
ImmutableSet<Taclet> |
ClassAxiomImpl.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
QueryAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
PartialInvAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ContractAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
RepresentsAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ModelMethodExecution.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
Modifier and Type | Method and Description |
---|---|
Pair<Label,Term> |
JmlTermFactory.createBreaks(Term term,
java.lang.String label) |
Pair<Label,Term> |
JmlTermFactory.createContinues(Term term,
java.lang.String label) |
Pair<IObserverFunction,Term> |
JmlTermFactory.represents(SLExpression lhs,
Term t) |
Pair<Label,Term> |
JmlIO.translateLabeledClause(LabeledParserRuleContext parserRuleContext,
OriginTermLabel.SpecType type)
Interpret a labeled term (breaks clauses, continue clauses).
|
Pair<IObserverFunction,Term> |
JmlIO.translateRepresents(LabeledParserRuleContext clause)
Interpret a given represents clause.
|
Pair<IObserverFunction,Term> |
JmlIO.translateRepresents(org.antlr.v4.runtime.ParserRuleContext clause)
Interpret the given parse tree as a represents clause
|
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.createUnionF(boolean nullable,
Pair<KeYJavaType,ImmutableList<LogicVariable>> declVars,
Term expr,
Term guard) |
Modifier and Type | Class and Description |
---|---|
protected static class |
SymbolicExecutionTreeBuilder.JavaPair
Utility class to group a call stack size with an
ImmutableList of SourceElement with the elements of interest. |
Modifier and Type | Method and Description |
---|---|
protected Pair<java.lang.Boolean,ImmutableList<Term>> |
ExecutionVariableExtractor.updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects,
Term value)
Updates the already visited objects list if required.
|
Modifier and Type | Method and Description |
---|---|
static Pair<java.lang.Integer,SourceElement> |
SymbolicExecutionUtil.computeSecondStatement(RuleApp ruleApp)
Computes the call stack size and the second statement
similar to
NodeInfo.computeActiveStatement(SourceElement) . |
Pair<ImmutableList<Term>,Term> |
SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult.getUpdatesAndTerm()
Returns the updates.
|
Modifier and Type | Method and Description |
---|---|
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
Constructor and Description |
---|
ContractPostOrExcPostExceptionVariableResult(Term workingTerm,
Pair<ImmutableList<Term>,Term> updatesAndTerm,
Term exceptionDefinition,
Term exceptionEquality)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Pair<Sort,IObserverFunction>> |
MiscTools.collectObservers(Term t)
Recursively collect all observers for this term including all of its sub terms.
|
java.util.Iterator<Pair<K,V>> |
LinkedHashMap.iterator() |
Modifier and Type | Method and Description |
---|---|
static <S,T> java.util.Set<S> |
Pair.getFirstSet(java.util.Collection<Pair<S,T>> pairs)
Returns the set of first entries from a collection of pairs.
|
static <S,T> java.util.Set<T> |
Pair.getSecondSet(java.util.Collection<Pair<S,T>> pairs)
Returns the set of second entries from a collection of pairs.
|
static <S,T> java.util.Map<S,T> |
Pair.toMap(java.util.Collection<Pair<S,T>> pairs)
Convert a collection of pairs into a map.
|
Modifier and Type | Class and Description |
---|---|
class |
SymbolicExecutionState
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
Modifier and Type | Method and Description |
---|---|
static Pair<SymbolicExecutionState,SymbolicExecutionState> |
MergeRuleUtils.handleNameClashes(SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Services services)
Due to the introduction of local namespaces, we run into trouble when
applying state merging in the presence of locally introduced symbols.
|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
boolean registerInNamespaces,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
Modifier and Type | Method and Description |
---|---|
static MergeRuleUtils.Option<Pair<Term,Term>> |
MergeRuleUtils.getDistinguishingFormula(java.util.ArrayList<Term> conjElemsPathCond1,
java.util.ArrayList<Term> conjElemsPathCond2,
Services services) |
static MergeRuleUtils.Option<Pair<Term,Term>> |
MergeRuleUtils.getDistinguishingFormula(Term pathCondition1,
Term pathCondition2,
Services services)
Computes a formula that implies pathCondition1 and, if pathCondition1 and
pathCondition2 are contradicting, does not imply pathCondition2.
|
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
MergeRuleUtils.parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
Copyright © 2003-2019 The KeY-Project.