Package | Description |
---|---|
de.uka.ilkd.key.nparser | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.strategy.definition | |
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Triple<java.lang.String,java.lang.Integer,java.lang.Integer> |
KeyAst.File.findProofScript() |
Modifier and Type | Method and Description |
---|---|
Triple<java.lang.String,java.lang.Integer,java.lang.Integer> |
KeYUserProblemFile.readProofScript() |
Modifier and Type | Method and Description |
---|---|
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
MergeRule.mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
Modifier and Type | Method and Description |
---|---|
DependencyContract |
ContractFactory.dep(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
Modifier and Type | Method and Description |
---|---|
Triple<LabeledParserRuleContext,LabeledParserRuleContext,LabeledParserRuleContext>[] |
TextualJMLSpecCase.getAbbreviations() |
Modifier and Type | Method and Description |
---|---|
Triple<IObserverFunction,Term,Term> |
JmlTermFactory.depends(SLExpression lhs,
Term rhs,
SLExpression mby) |
Triple<IObserverFunction,Term,Term> |
JmlIO.translateDependencyContract(LabeledParserRuleContext ctx)
Translates a dependency contract.
|
Triple<IObserverFunction,Term,Term> |
JmlIO.translateDependencyContract(org.antlr.v4.runtime.ParserRuleContext ctx)
Translates the given context into a dependency contract, aka, accessible-clause or depends-clause.
|
Modifier and Type | Method and Description |
---|---|
java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> |
StrategySettingsDefinition.getFurtherDefaults() |
Constructor and Description |
---|
StrategySettingsDefinition(boolean showMaxRuleApplications,
java.lang.String maxRuleApplicationsLabel,
int defaultMaxRuleApplications,
java.lang.String propertiesTitle,
IDefaultStrategyPropertiesFactory defaultPropertiesFactory,
java.util.ArrayList<Triple<java.lang.String,java.lang.Integer,IDefaultStrategyPropertiesFactory>> furtherDefaults,
AbstractStrategyPropertyDefinition... properties)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
AbstractSideProofRule.computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
SymbolicExecutionSideProofUtil.computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
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 and conditions. |
Modifier and Type | Class and Description |
---|---|
class |
SymbolicExecutionStateWithProgCnt
A symbolic execution state with program counter is a triple of a symbolic
state in form of a parallel update, a path condition in form of a JavaDL
formula, and a program counter in form of a JavaDL formula with non-empty
Java Block (and a possible post condition as first, and only, sub term).
|
Copyright © 2003-2019 The KeY-Project.