Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
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 |
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.init |
This package contains classes handling prover initialisation.
|
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.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
ClassTree.getDisplayName(Services services,
IObserverFunction ov)
Returns a human readable display name for the given
ObserverFunction
with use of the given Services . |
void |
ClassTree.select(KeYJavaType kjt,
IObserverFunction target) |
static void |
ProofManagementDialog.showInstance(InitConfig initConfig,
KeYJavaType selectedKJT,
IObserverFunction selectedTarget)
Shows the dialog and selects the passed
KeYJavaType and its
IObserverFunction . |
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 |
---|---|
IObserverFunction |
JavaInfo.getInv()
Returns the special symbol
<inv> which stands for the class invariant of an object. |
IObserverFunction |
JavaInfo.getStaticInv(KeYJavaType target)
Returns the special symbol
<staticInv> which stands for the static invariant of a type. |
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.func(IObserverFunction f,
Term... s) |
ImmutableList<ProgramVariable> |
TermBuilder.paramVars(IObserverFunction obs,
boolean makeNamesUnique)
Creates program variables for the parameters.
|
ImmutableList<ProgramVariable> |
TermBuilder.paramVars(java.lang.String postfix,
IObserverFunction obs,
boolean makeNamesUnique)
Creates program variables for the parameters.
|
Modifier and Type | Interface and Description |
---|---|
interface |
IProgramMethod |
Modifier and Type | Class and Description |
---|---|
class |
ObserverFunction
Objects of this class represent "observer" function or predicate symbols.
|
class |
ProgramMethod
The program method represents a (pure) method in the logic.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Modifier and Type | Field and Description |
---|---|
IObserverFunction |
ObserverWithType.obs |
Constructor and Description |
---|
ObserverWithType(KeYJavaType kjt,
IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
IObserverFunction |
WellDefinednessPO.getTarget() |
Modifier and Type | Method and Description |
---|---|
IObserverFunction |
SpecificationRepository.getTargetOfProof(Proof proof)
Returns the target that the passed proof is about, or null.
|
IObserverFunction |
SpecificationRepository.unlimitObs(IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<IObserverFunction> |
SpecificationRepository.getContractTargets(KeYJavaType kjt)
Returns all functions for which contracts are registered in the passed
type.
|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
SpecificationRepository.getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
Pair<IObserverFunction,ImmutableSet<Taclet>> |
SpecificationRepository.limitObs(IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
boolean |
ProofCorrectnessMgt.contractApplicableFor(KeYJavaType kjt,
IObserverFunction target)
Deprecated.
|
ImmutableSet<Contract> |
SpecificationRepository.getContracts(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) contracts for the passed target.
|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
SpecificationRepository.getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
ImmutableSet<Proof> |
SpecificationRepository.getProofs(KeYJavaType kjt,
IObserverFunction target)
Returns all proofs registered for the passed target and its overriding
targets.
|
Pair<IObserverFunction,ImmutableSet<Taclet>> |
SpecificationRepository.limitObs(IObserverFunction obs) |
IObserverFunction |
SpecificationRepository.unlimitObs(IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
IObserverFunction |
UseDependencyContractApp.getObserverFunction(Services services) |
abstract IObserverFunction |
AbstractContractRuleApp.getObserverFunction(Services services) |
IObserverFunction |
ContractRuleApp.getObserverFunction(Services services) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Contract> |
UseDependencyContractRule.getApplicableContracts(Services services,
KeYJavaType kjt,
IObserverFunction target)
Returns the dependency contracts which are applicable for the passed
target.
|
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) |
Taclet |
TacletGenerator.generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
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 IObserverFunction |
ClassAxiom.getTarget()
Returns the axiomatised function symbol.
|
IObserverFunction |
ClassAxiomImpl.getTarget()
Class axioms do not have targets (in opposition to represents clauses)
|
IObserverFunction |
QueryAxiom.getTarget() |
IObserverFunction |
PartialInvAxiom.getTarget() |
IObserverFunction |
ContractAxiom.getTarget() |
IObserverFunction |
DependencyContractImpl.getTarget() |
IObserverFunction |
WellDefinednessCheck.getTarget() |
IObserverFunction |
RepresentsAxiom.getTarget() |
IObserverFunction |
Contract.getTarget()
Returns the contracted function symbol.
|
IObserverFunction |
ModelMethodExecution.getTarget() |
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 |
---|---|
DependencyContract |
ContractFactory.dep(KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
DependencyContract |
ContractFactory.dep(java.lang.String string,
KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
static java.lang.String |
ContractFactory.generateContractName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
static java.lang.String |
ContractFactory.generateContractTypeName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn) |
static java.lang.String |
ContractFactory.generateDisplayName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
MethodWellDefinedness |
MethodWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalOperationContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
ClassWellDefinedness |
ClassWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopContract |
LoopContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
InformationFlowContract |
InformationFlowContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalBlockContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
InformationFlowContract |
InformationFlowContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Return a new contract which equals this contract except that the
the KeYJavaType and ObserverFunction are set to the new values.
|
LoopSpecification |
LoopSpecification.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
DependencyContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
BlockContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
Contract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Returns a contract which is identical to this contract except that the KeYJavaType and
IObserverFunction are set to the new values.
|
Contract |
LoopWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
BlockContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopContract |
LoopContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
BlockWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalLoopContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
AuxiliaryContract |
AuxiliaryContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopSpecification |
LoopSpecImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Modifier and Type | Method and Description |
---|---|
Triple<IObserverFunction,Term,Term> |
JmlTermFactory.depends(SLExpression lhs,
Term rhs,
SLExpression mby) |
Pair<IObserverFunction,Term> |
JmlTermFactory.represents(SLExpression lhs,
Term t) |
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.
|
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 |
---|---|
static ImmutableSet<Pair<Sort,IObserverFunction>> |
MiscTools.collectObservers(Term t)
Recursively collect all observers for this term including all of its sub terms.
|
Copyright © 2003-2019 The KeY-Project.