Package | Description |
---|---|
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.rule.conditions | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.dl.translation | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.strategy.quantifierHeuristics |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.var(ParsableVariable v) |
Modifier and Type | Interface and Description |
---|---|
interface |
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
interface |
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
interface |
UpdateableOperator
Operators implementing this interface may stand for
locations as well.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractSV
Abstract base class for schema variables.
|
class |
FormulaSV
A schema variable that is used as placeholder for formulas.
|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
class |
ModalOperatorSV
Schema variable matching modal operators.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
ProgramVariable
The objects of this class represent program variables and program
constants (resulting from static final declarations in programs; TODO: it is
weird that constants are a special case of variables).
|
class |
SkolemTermSV
Schema variable that is instantiated with fresh Skolem constants.
|
class |
TermLabelSV
A schema variable which matches term labels
|
class |
TermSV
A schema variable that is used as placeholder for terms.
|
class |
UpdateSV
A schema variable that is used as placeholder for updates.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
Constructor and Description |
---|
IsThisReference(ParsableVariable var,
boolean negation) |
SameObserverCondition(ParsableVariable schema1,
ParsableVariable schema2)
Create a new condition
|
Modifier and Type | Method and Description |
---|---|
Term |
RepresentsAxiom.getAxiom(ParsableVariable heapVar,
ParsableVariable selfVar,
Services services) |
Term |
InitiallyClauseImpl.getClause(ParsableVariable selfVar,
TermServices services) |
Term |
InitiallyClause.getClause(ParsableVariable selfVar,
TermServices services)
Returns the formula without implicit all-quantification over
the receiver object.
|
Term |
ClassInvariantImpl.getInv(ParsableVariable selfVar,
TermServices services) |
Term |
ClassInvariant.getInv(ParsableVariable selfVar,
TermServices services)
Returns the invariant formula without implicit all-quantification over
the receiver object.
|
Term |
WellDefinednessCheck.getPost(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition post,
ParsableVariable result,
TermServices services)
Gets the full valid post-condition
|
WellDefinednessCheck.TermAndFunc |
WellDefinednessCheck.getPre(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition pre,
ParsableVariable self,
ParsableVariable heap,
ImmutableList<? extends ParsableVariable> parameters,
boolean taclet,
Services services)
Gets the full valid precondition, which holds in the element's pre-state.
|
Modifier and Type | Method and Description |
---|---|
WellDefinednessCheck.TermAndFunc |
WellDefinednessCheck.getPre(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition pre,
ParsableVariable self,
ParsableVariable heap,
ImmutableList<? extends ParsableVariable> parameters,
boolean taclet,
Services services)
Gets the full valid precondition, which holds in the element's pre-state.
|
Constructor and Description |
---|
ClassInvariantImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar)
Creates a class invariant.
|
InitiallyClauseImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar,
LabeledParserRuleContext originalSpec)
Creates a class invariant.
|
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
DLSpecFactory.createDLClassInvariant(java.lang.String name,
java.lang.String displayName,
ParsableVariable selfVar,
Term inv)
Creates a class invariant from a formula and a designated "self".
|
Constructor and Description |
---|
JMLResolverManager(JavaInfo javaInfo,
KeYJavaType specInClass,
ParsableVariable selfVar,
SLExceptionFactory eManager) |
Modifier and Type | Method and Description |
---|---|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ParsableVariable pv,
KeYJavaType kjt)
Puts a local variable into the topmost namespace on the stack
|
Constructor and Description |
---|
SLResolverManager(SLExceptionFactory excManager,
KeYJavaType specInClass,
ParsableVariable selfVar,
boolean useLocalVarsAsImplicitReceivers,
TermBuilder tb) |
Modifier and Type | Class and Description |
---|---|
class |
Metavariable
Deprecated.
|
Copyright © 2003-2019 The KeY-Project.