Modifier and Type | Class and Description |
---|---|
class |
AbstractDomainElement
An element of an abstract domain.
|
Modifier and Type | Class and Description |
---|---|
class |
BooleanDomainElem
A domain element of the simple boolean lattice.
|
class |
False
The False element of the boolean lattice, representing
exactly the boolean false.
|
class |
True
The True element of the boolean lattice, representing
exactly the boolean true.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractionPredicate
Interface for predicates used for predicate abstraction.
|
class |
AbstractPredicateAbstractionDomainElement
A base class for abstract domain elements in a predicate abstraction lattice.
|
class |
ConjunctivePredicateAbstractionDomainElement
An abstract domain element for a predicate abstraction lattice based on the
conjunction of predicates.
|
class |
DisjunctivePredicateAbstractionDomainElement
An abstract domain element for a predicate abstraction lattice based on the
disjunction of predicates.
|
class |
SimplePredicateAbstractionDomainElement
An abstract domain element for a predicate abstraction lattice encapsulating
exactly one abstraction predicate.
|
Modifier and Type | Class and Description |
---|---|
class |
Bottom
The Bottom element of the sign lattice, representing
no number at all.
|
class |
Geq
The Geq element of the sign lattice, representing
all positive integers and zero.
|
class |
Leq
The Leq element of the sign lattice, representing
all negative numbers and zero.
|
class |
Neg
The Neg element of the sign lattice, representing
all strictly negative integers.
|
class |
Pos
The Pos element of the sign lattice, representing
all strictly positive numbers.
|
class |
SignAnalysisDomainElem
A domain element for sign analysis.
|
class |
Top
The Top element of the sign lattice, representing
all integers.
|
class |
Zero
The Zero element of the sign lattice, representing
only the number 0.
|
Modifier and Type | Class and Description |
---|---|
protected class |
UseInformationFlowContractMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Modifier and Type | Method and Description |
---|---|
void |
InfFlowProofSymbols.add(Named symb) |
void |
LoopInvExecutionPO.addIFSymbol(Named n) |
void |
InfFlowPO.addIFSymbol(Named n) |
void |
InfFlowContractPO.addIFSymbol(Named n) |
void |
BlockExecutionPO.addIFSymbol(Named n) |
void |
SymbolicExecutionPO.addIFSymbol(Named n) |
void |
InfFlowProofSymbols.addLabeled(Named symb) |
void |
LoopInvExecutionPO.addLabeledIFSymbol(Named n) |
void |
InfFlowPO.addLabeledIFSymbol(Named n) |
void |
InfFlowContractPO.addLabeledIFSymbol(Named n) |
void |
BlockExecutionPO.addLabeledIFSymbol(Named n) |
void |
SymbolicExecutionPO.addLabeledIFSymbol(Named n) |
Modifier and Type | Class and Description |
---|---|
class |
InfFlowProof
The proof object used by Information Flow Proofs.
|
Modifier and Type | Class and Description |
---|---|
class |
InfFlowContractAppTaclet
A normal RewriteTaclet except that the formula which is added by this taclet
is also added to the list of formulas contained in the
INF_FLOW_CONTRACT_APPL_PROPERTY.
|
Modifier and Type | Class and Description |
---|---|
class |
BooleanLDT
This class inherits from LDT and implements all method that are
necessary to handle the primitive type boolean.
|
class |
CharListLDT |
class |
DoubleLDT
Complete this class if you want to add support for the Java double type.
|
class |
FloatLDT
Complete this class if you want to add support for the Java float type.
|
class |
FreeLDT
Generic data type, which has no predefined theory.
|
class |
HeapLDT
LDT responsible for the "Heap" sort, and the associated "Field" sort.
|
class |
IntegerLDT
This class inherits from LDT and implements all method that are
necessary to handle integers, shorts and bytes.
|
class |
LDT
An "LDT" or "language data type" class corresponds to a standard rule file
shipped with KeY.
|
class |
LocSetLDT |
class |
MapLDT
LDT for maps.
|
class |
PermissionLDT |
class |
RealLDT
Complete this class if you want to add support for the JML \real type.
|
class |
SeqLDT |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
HeapLDT.getPrettyFieldName(Named fieldSymbol)
Given a constant symbol representing a field, this method returns a
simplified name of the constant symbol to be used for pretty printing.
|
Modifier and Type | Class and Description |
---|---|
class |
Namespace<E extends Named>
A Namespace keeps track of already used
Name s and the objects
carrying these names. |
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 | Class and Description |
---|---|
class |
Choice
A choice is an option in a category.
|
Modifier and Type | Method and Description |
---|---|
Named |
NamespaceSet.lookup(Name name)
looks up if the given name is found in one of the namespaces
and returns the named object or null if no object with the same name
has been found
|
Named |
NamespaceSet.lookupLogicSymbol(Name name)
looks up for the symbol in the namespaces sort, functions and
programVariables
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.Iterable<ProgramElementName> |
VariableNamer.wrapGlobals(ImmutableList<? extends Named> globals)
creates a Globals object for use with other internal methods
|
Modifier and Type | Interface and Description |
---|---|
interface |
TermLabel
The interface for term labels.
|
Modifier and Type | Class and Description |
---|---|
class |
BlockContractValidityTermLabel
Label attached to the modality of the validity branch of a block contract.
|
class |
FormulaTermLabel
Label attached to a predicates for instance in postconditions, loop invariants or precondition checks of applied operation contracts.
|
class |
OriginTermLabel
An
OriginTermLabel saves a term's origin in the JML specification
(OriginTermLabel.getOrigin() ) as well as the origins of all of its subterms and former
subterms (OriginTermLabel.getSubtermOrigins() ). |
class |
ParameterlessTermLabel
The Class
ParameterlessTermLabel can be used to define labels without parameters. |
class |
SymbolicExecutionTermLabel
Label attached to a symbolic execution thread.
|
Modifier and Type | Interface and Description |
---|---|
interface |
IObserverFunction |
interface |
IProgramMethod |
interface |
IProgramVariable |
interface |
Operator
All symbols acting as members of a term e.g.
|
interface |
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
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 |
SortedOperator
Operator with well-defined argument and result sorts.
|
interface |
TermTransformer
TermTransformer perform complex term transformation which cannot be
(efficiently or at all) described by taclets.
|
interface |
UpdateableOperator
Operators implementing this interface may stand for
locations as well.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
class |
AbstractSV
Abstract base class for schema variables.
|
class |
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
class |
ElementaryUpdate
Class of operators for elementary updates, i.e., updates of the form
"x := t".
|
class |
Equality
This class defines the equality operator "=".
|
class |
FormulaSV
A schema variable that is used as placeholder for formulas.
|
class |
Function
Objects of this class represent function and predicate symbols.
|
class |
IfExThenElse
This singleton class implements a conditional operator
"\ifEx iv; (phi) \then (t1) \else (t2)", where iv is an integer logic
variable, phi is a formula, and where t1 and t2 are terms with the same sort.
|
class |
IfThenElse
This singleton class implements a general conditional operator
\if (phi) \then (t1) \else (t2).
|
class |
Junctor
Class of junctor operators, i.e., operators connecting
a given number of formula to create another formula.
|
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 |
Modality
This class is used to represent a dynamic logic modality like
diamond and box (but also extensions of DL like
preserves and throughout are possible in the future).
|
class |
ModalOperatorSV
Schema variable matching modal operators.
|
class |
ObserverFunction
Objects of this class represent "observer" function or predicate symbols.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
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.
|
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 |
Quantifier
The two objects of this class represent the universal and the existential
quantifier, respectively.
|
class |
SkolemTermSV
Schema variable that is instantiated with fresh Skolem constants.
|
class |
SortDependingFunction
The objects of this class represent families of function symbols, where
each family contains an instantiation of a template symbol for a particular
sort.
|
class |
SubstOp
Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators.
|
class |
TermLabelSV
A schema variable which matches term labels
|
class |
TermSV
A schema variable that is used as placeholder for terms.
|
class |
Transformer
Functions with a restricted/special rule set only applicable for the top level
of the term transformer and not directly for its arguments, prohibiting any rule
applications to sub arguments as well as applications from outside such as update applications.
|
class |
UpdateApplication
Singleton class defining a binary operator {u}t that applies updates u to
terms, formulas, or other updates t.
|
class |
UpdateJunctor
Class of update junctor operators, i.e., operators connecting
a given number of updates to create another update.
|
class |
UpdateSV
A schema variable that is used as placeholder for updates.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
class |
WarySubstOp |
Modifier and Type | Interface and Description |
---|---|
interface |
Sort |
Modifier and Type | Class and Description |
---|---|
class |
AbstractSort
Abstract base class for implementations of the Sort interface.
|
class |
ArraySort
The objects of this class represent array sorts (in the sense of *Java*
arrays).
|
class |
GenericSort
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
class |
NullSort
There is one instance of this class per proof, representing the sort "Null".
|
class |
ProgramSVSort
Special "sorts" used for schema variables matching program constructs
(class ProgramSV).
|
static class |
ProgramSVSort.SimpleExpressionNonStringObjectSort
This sort represents a type of program schema variables that match
on non string object variables.
|
static class |
ProgramSVSort.SimpleExpressionStringSort
This sort represents a type of program schema variables that match
on string literals and string variables.
|
class |
ProxySort |
class |
SortImpl
Standard implementation of the Sort interface.
|
Modifier and Type | Class and Description |
---|---|
class |
FilterStrategy |
protected class |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Modifier and Type | Method and Description |
---|---|
protected Named |
DefaultBuilder.lookup(Name n) |
Modifier and Type | Class and Description |
---|---|
class |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Modifier and Type | Class and Description |
---|---|
class |
AntecTaclet
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
class |
FindTaclet
An abstract class to represent Taclets with a find part.
|
class |
NoFindTaclet
Used to implement a Taclet that has no find part.
|
class |
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
class |
RuleSet |
class |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
class |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
Modifier and Type | Class and Description |
---|---|
class |
AddCast |
class |
ArrayBaseInstanceOf
Creates an Type::instance(..) term for the component type of the
array.
|
class |
ConstantValue
Replace a program variable that is a compile-time constant with the
value of the initializer
|
class |
CreateBeforeLoopUpdate
Initializes the "before loop" update needed for the assignable clause.
|
class |
CreateFrameCond
Creates the frame condition (aka "assignable clause") for the given loop.
|
class |
CreateHeapAnonUpdate
Creates the anonymizing update for the heap.
|
class |
CreateLocalAnonUpdate
Expects a loop body and creates the anonymizing update
out_1:=anon_1||...||out_n:=anon_n , where anon_1, ..., anon_n are
the written variables in the loop body visible to the outside. |
class |
CreateWellformedCond
Creates the wellformedness condition for the given anonymizing heap terms if
they apply for the current profile and modality type.
|
class |
EnumConstantValue
resolve a program variable to an integer literal.
|
class |
ExpandQueriesMetaConstruct
Uses the class
QueryExpand in order to insert query expansions in the term that the
meta construct is applied on. |
class |
IntroAtPreDefsOp |
class |
MemberPVToField |
class |
ObserverEqualityMetaConstruct
This meta contruct allows one to prove equality (equivalence) of two
observer terms if they belong to the same observer function symbol.
|
Modifier and Type | Class and Description |
---|---|
class |
DivideLCRMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
DivideMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
MetaAdd |
class |
MetaArithBitMaskOp |
class |
MetaBinaryAnd |
class |
MetaBinaryOr |
class |
MetaBinaryXOr |
class |
MetaDiv |
class |
MetaEqual |
class |
MetaGeq |
class |
MetaGreater |
class |
MetaLeq |
class |
MetaLess |
class |
MetaMul |
class |
MetaPow
Computes the pow function for literals.
|
class |
MetaShift |
class |
MetaShiftLeft |
class |
MetaShiftRight |
class |
MetaSub |
Modifier and Type | Interface and Description |
---|---|
interface |
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
interface |
StrategyFactory
Interface for creating Strategy instances.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractFeatureStrategy |
class |
FIFOStrategy
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
static class |
FIFOStrategy.Factory |
class |
JavaCardDLStrategy
Strategy tailored to be used as long as a java program can be found in the
sequent.
|
class |
JavaCardDLStrategyFactory |
class |
SimpleFilteredStrategy
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
Modifier and Type | Class and Description |
---|---|
class |
Metavariable
Deprecated.
|
Modifier and Type | Class and Description |
---|---|
class |
SimplifyTermStrategy
|
static class |
SimplifyTermStrategy.Factory
The
StrategyFactory to create instances of SimplifyTermStrategy . |
class |
SymbolicExecutionStrategy
Strategy to use for symbolic execution. |
static class |
SymbolicExecutionStrategy.Factory
The
StrategyFactory to create instances of SymbolicExecutionStrategy . |
Modifier and Type | Method and Description |
---|---|
void |
UserDefinedSymbols.addSort(Named symbol) |
Copyright © 2003-2019 The KeY-Project.