Package | Description |
---|---|
de.uka.ilkd.key.core | |
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
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.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
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.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Namespace<Function> |
KeYMediator.func_ns()
returns the function namespace
|
Modifier and Type | Method and Description |
---|---|
Function |
DLEmbeddedExpression.getFunctionSymbol() |
Constructor and Description |
---|
DLEmbeddedExpression(Function f,
ExtList children) |
Modifier and Type | Field and Description |
---|---|
Function |
MapLDT.mapEmpty |
Modifier and Type | Method and Description |
---|---|
protected Function |
LDT.addFunction(Function f)
adds a function to the LDT
|
protected Function |
LDT.addFunction(TermServices services,
java.lang.String funcName)
looks up a function in the namespace and adds it to the LDT
|
Function |
HeapLDT.getAcc() |
Function |
IntegerLDT.getAdd() |
Function |
LocSetLDT.getAllFields() |
Function |
LocSetLDT.getAllLocs() |
Function |
LocSetLDT.getAllObjects() |
Function |
HeapLDT.getAnon() |
Function |
IntegerLDT.getArithJavaIntAddition()
returns the function symbol interpreted as the Java addition on
int (or promotabel to int) operators, i.e.
|
Function |
IntegerLDT.getArithModulo()
returns the function symbol used to represent the modulo operation of
the arithmetical integers
|
Function |
IntegerLDT.getArithModuloByte()
maps an integer back into byte range
|
Function |
IntegerLDT.getArithModuloChar()
maps an integer back into char range
|
Function |
IntegerLDT.getArithModuloInt()
maps an integer back into int range
|
Function |
IntegerLDT.getArithModuloLong()
maps an integer back into long range
|
Function |
IntegerLDT.getArithModuloShort()
maps an integer back into long range
|
Function |
HeapLDT.getArr() |
Function |
LocSetLDT.getArrayRange() |
Function |
FreeLDT.getAtom() |
Function |
IntegerLDT.getBitwiseOrJavaInt()
returns the function symbol representing the bitwise-or for Java int
|
Function |
IntegerLDT.getBprod() |
Function |
IntegerLDT.getBsum() |
Function |
IntegerLDT.getCharSymbol() |
Function |
HeapLDT.getClassErroneous(Sort instanceSort,
TermServices services) |
Function |
HeapLDT.getClassInitializationInProgress(Sort instanceSort,
TermServices services) |
Function |
HeapLDT.getClassInitialized(Sort instanceSort,
TermServices services) |
Function |
HeapLDT.getClassPrepared(Sort instanceSort,
TermServices services) |
Function |
CharListLDT.getClContains() |
Function |
CharListLDT.getClEndsWith() |
Function |
CharListLDT.getClHashCode() |
Function |
CharListLDT.getClIndexOfChar() |
Function |
CharListLDT.getClIndexOfCl() |
Function |
CharListLDT.getClLastIndexOfChar() |
Function |
CharListLDT.getClLastIndexOfCl() |
Function |
CharListLDT.getClRemoveZeros() |
Function |
CharListLDT.getClReplace() |
Function |
CharListLDT.getClStartsWith() |
Function |
CharListLDT.getClTranslateInt() |
Function |
HeapLDT.getCreate() |
Function |
HeapLDT.getCreated() |
Function |
LocSetLDT.getCreatedInHeap() |
Function |
LocSetLDT.getDisjoint() |
Function |
IntegerLDT.getDiv() |
Function |
LocSetLDT.getElementOf() |
Function |
LocSetLDT.getEmpty() |
Function |
BooleanLDT.getFalseConst()
returns the function representing the boolean value FALSE
|
Function |
HeapLDT.getFieldSymbolForPV(LocationVariable fieldPV,
Services services)
Given a "program variable" representing a field or a model field,
returns the function symbol representing the same field.
|
Function |
LocSetLDT.getFreshLocs() |
Function |
DoubleLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
CharListLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FreeLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
MapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
RealLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
BooleanLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
PermissionLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
LocSetLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
IntegerLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
null if no function is found for the given operator
|
Function |
HeapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FloatLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
SeqLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
abstract Function |
LDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec)
returns the function symbol for the given operation
|
Function |
IntegerLDT.getGreaterOrEquals() |
Function |
IntegerLDT.getGreaterThan() |
Function |
IntegerLDT.getInBounds(Type t) |
Function |
IntegerLDT.getIndex()
Placeholder for the loop index variable in an enhanced for loop over arrays.
|
Function |
LocSetLDT.getInfiniteUnion() |
Function |
HeapLDT.getInitialized() |
Function |
LocSetLDT.getIntersect() |
Function |
IntegerLDT.getJavaAddInt()
the function representing the Java operator when one of the
operators is an or can be promoted to an int
|
Function |
IntegerLDT.getJavaAddLong()
the function representing the Java operator when one of the
operators is of type long
|
Function |
IntegerLDT.getJavaBitwiseAndInt()
the function representing the Java operator when one of the
operators is an or can be promoted to int
|
Function |
IntegerLDT.getJavaBitwiseAndLong()
the function representing the Java operator when one of the
operators is of type long
|
Function |
IntegerLDT.getJavaBitwiseNegation()
the function representing the Java operator
~ |
Function |
IntegerLDT.getJavaBitwiseOrInt()
the function representing the Java operator
|
when one of the operands is an or can be promoted to int |
Function |
IntegerLDT.getJavaBitwiseOrLong()
the function representing the Java operator
|
when one of the operands is of type long |
Function |
IntegerLDT.getJavaBitwiseXOrInt()
the function representing the Java operator
^
when one of the operands is an or can be promoted to int |
Function |
IntegerLDT.getJavaBitwiseXOrLong()
the function representing the Java operator
^
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaCast(Type t) |
Function |
IntegerLDT.getJavaCastByte()
the function representing the Java operator
(byte) |
Function |
IntegerLDT.getJavaCastChar()
the function representing the Java operator
(char) |
Function |
IntegerLDT.getJavaCastInt()
the function representing the Java operator
(int) |
Function |
IntegerLDT.getJavaCastLong()
the function representing the Java operator
(long) |
Function |
IntegerLDT.getJavaCastShort()
the function representing the Java operator
(short) |
Function |
IntegerLDT.getJavaDivInt()
the function representing the Java operator
/
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaDivLong()
the function representing the Java operator
/
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaMod()
the function representing the Java operator
%
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaMulInt()
the function representing the Java operator
*
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaMulLong()
the function representing the Java operator
*
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaShiftLeftInt()
the function representing the Java operator
<<
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaShiftLeftLong()
the function representing the Java operator
<<
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaShiftRightInt()
the function representing the Java operator
>>
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaShiftRightLong()
the function representing the Java operator
>>
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaSubInt()
the function representing the Java operator
-
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaSubLong()
the function representing the Java operator
-
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaUnaryMinusInt()
the function representing the Java operator
-expr
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaUnaryMinusLong()
the function representing the Java operator
-exprLong
when one of the operands is exact of type long |
Function |
IntegerLDT.getJavaUnsignedShiftRightInt()
the function representing the Java operator
>>>
when one of the operands is an or a subtype of int |
Function |
IntegerLDT.getJavaUnsignedShiftRightLong()
the function representing the Java operator
>>>
when one of the operands is exact of type long |
Function |
IntegerLDT.getJDivision()
returns the function symbol used to represent java-like division of
the arithmetical integers
|
Function |
IntegerLDT.getJModulo()
returns the function symbol used to represent the java-like modulo operation of
the arithmetical integers
|
Function |
HeapLDT.getLength() |
Function |
IntegerLDT.getLessOrEquals() |
Function |
IntegerLDT.getLessThan() |
Function |
MapLDT.getMapEmpty() |
Function |
HeapLDT.getMemset() |
Function |
IntegerLDT.getMod() |
Function |
IntegerLDT.getModuloLong()
returns a function mapping an arithmetic integer to its Java long representation
|
Function |
IntegerLDT.getMul() |
Function |
IntegerLDT.getNeg() |
Function |
IntegerLDT.getNegativeNumberSign() |
Function |
HeapLDT.getNull() |
Function |
IntegerLDT.getNumberLiteralFor(int number) |
Function |
IntegerLDT.getNumberSymbol() |
Function |
IntegerLDT.getNumberTerminator() |
Function |
PermissionLDT.getPermissionsFor() |
Function |
IntegerLDT.getPow() |
Function |
HeapLDT.getPrec() |
Function |
HeapLDT.getReach() |
Function |
SeqLDT.getSeqConcat() |
Function |
SeqLDT.getSeqDef() |
Function |
SeqLDT.getSeqEmpty() |
Function |
SeqLDT.getSeqIndexOf() |
Function |
SeqLDT.getSeqLen() |
Function |
SeqLDT.getSeqReverse() |
Function |
SeqLDT.getSeqSingleton() |
Function |
SeqLDT.getSeqSub() |
Function |
LocSetLDT.getSetMinus() |
Function |
LocSetLDT.getSingleton() |
Function |
HeapLDT.getStore() |
Function |
IntegerLDT.getSub() |
Function |
LocSetLDT.getSubset() |
Function |
BooleanLDT.getTrueConst()
returns the function representing the boolean value TRUE
|
Function |
LocSetLDT.getUnion() |
Function |
SeqLDT.getValues()
Placeholder for the sequence of values observed through the execution of an enhanced for loop.
|
Function |
HeapLDT.getWellFormed() |
Modifier and Type | Method and Description |
---|---|
protected Function |
LDT.addFunction(Function f)
adds a function to the LDT
|
boolean |
HeapLDT.containsFunction(Function op) |
boolean |
LDT.containsFunction(Function op) |
static java.lang.String |
HeapLDT.getClassName(Function fieldSymbol)
Extracts the name of the enclosing class from the name of a constant
symbol representing a field.
|
boolean |
DoubleLDT.hasLiteralFunction(Function f) |
boolean |
CharListLDT.hasLiteralFunction(Function f) |
boolean |
FreeLDT.hasLiteralFunction(Function f) |
boolean |
MapLDT.hasLiteralFunction(Function f) |
boolean |
RealLDT.hasLiteralFunction(Function f) |
boolean |
BooleanLDT.hasLiteralFunction(Function f) |
boolean |
PermissionLDT.hasLiteralFunction(Function f) |
boolean |
LocSetLDT.hasLiteralFunction(Function f) |
boolean |
IntegerLDT.hasLiteralFunction(Function f) |
boolean |
HeapLDT.hasLiteralFunction(Function f) |
boolean |
FloatLDT.hasLiteralFunction(Function f) |
boolean |
SeqLDT.hasLiteralFunction(Function f) |
abstract boolean |
LDT.hasLiteralFunction(Function f) |
Modifier and Type | Method and Description |
---|---|
Function |
TermBuilder.getMeasuredByEmpty() |
Modifier and Type | Method and Description |
---|---|
Namespace<Function> |
NamespaceSet.functions() |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.dot(Sort asSort,
Term o,
Function f) |
Term |
TermBuilder.fieldStore(TermServices services,
Term o,
Function f,
Term v) |
Term |
TermBuilder.func(Function f) |
Term |
TermBuilder.func(Function f,
Term... s) |
Term |
TermBuilder.func(Function f,
Term s) |
Term |
TermBuilder.func(Function f,
Term[] s,
ImmutableArray<QuantifiableVariable> boundVars) |
Term |
TermBuilder.func(Function f,
Term s1,
Term s2) |
Term |
TermBuilder.staticDot(Sort asSort,
Function f) |
Term |
TermBuilder.staticFieldStore(Function f,
Term v) |
Modifier and Type | Method and Description |
---|---|
void |
NamespaceSet.setFunctions(Namespace<Function> funcNS) |
Constructor and Description |
---|
NamespaceSet(Namespace<QuantifiableVariable> varNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS,
Namespace<RuleSet> ruleSetNS,
Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) |
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 |
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 |
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.
|
Modifier and Type | Method and Description |
---|---|
Function |
Function.rename(Name newName) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<Function> |
DefaultBuilder.functions() |
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
Namespace<QuantifiableVariable> var_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns,
Namespace<IProgramVariable> progVar_ns,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Constructor and Description |
---|
SeqConcatNotation(Function seqConcat,
Function seqSingleton,
Function charLiteral) |
Modifier and Type | Method and Description |
---|---|
java.lang.Iterable<Function> |
Node.getLocalFunctions()
Returns the set of freshly created function symbols known to this node.
|
Modifier and Type | Method and Description |
---|---|
void |
Node.addLocalFunctions(java.util.Collection<? extends Function> elements) |
Modifier and Type | Method and Description |
---|---|
Namespace<Function> |
InitConfig.funcNS()
returns the function namespace of this initial configuration.
|
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractPO.register(Function f,
Services services) |
Modifier and Type | Method and Description |
---|---|
static Term |
IntermediateProofReplayer.parseTerm(java.lang.String value,
Proof proof,
Namespace<QuantifiableVariable> varNS,
Namespace<IProgramVariable> progVarNS,
Namespace<Function> functNS)
Parses a given term in String representation.
|
Modifier and Type | Method and Description |
---|---|
protected static java.util.Map<LocationVariable,Function> |
AbstractBlockContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
BlockContract contract,
TermServices services) |
protected java.util.Map<LocationVariable,Function> |
AbstractLoopContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
LoopContract contract,
TermServices services) |
Namespace<Function> |
TacletApp.extendedFunctionNameSpace(Namespace<Function> func_ns)
create a new function namespace by adding all newly instantiated skolem
symbols to a new namespace.
|
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpWdGoal(Goal goal,
BlockContract contract,
Term update,
Term anonUpdate,
LocationVariable heap,
Function anonHeap,
ImmutableSet<ProgramVariable> localIns) |
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonInUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(java.util.Set<LocationVariable> vars,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildWellFormedAnonymisationHeapsCondition(java.util.Map<LocationVariable,Function> anonymisationHeaps) |
Namespace<Function> |
TacletApp.extendedFunctionNameSpace(Namespace<Function> func_ns)
create a new function namespace by adding all newly instantiated skolem
symbols to a new namespace.
|
protected AbstractBlockContractRule.InfFlowValidityData |
AbstractBlockContractRule.setUpInfFlowValidityGoal(Goal infFlowGoal,
BlockContract contract,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
Services services,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
java.util.List<LocationVariable> heaps,
ImmutableSet<ProgramVariable> localInVariables,
ImmutableSet<ProgramVariable> localOutVariables,
BlockContractInternalBuiltInRuleApp application,
AbstractAuxiliaryContractRule.Instantiation instantiation) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
Modifier and Type | Method and Description |
---|---|
Function |
AbstractSMTTranslator.FunctionWrapper.getFunction() |
Constructor and Description |
---|
FunctionWrapper(java.lang.StringBuffer name,
Function function) |
Modifier and Type | Field and Description |
---|---|
Function |
WellDefinednessCheck.TermAndFunc.func |
Modifier and Type | Method and Description |
---|---|
protected Function |
AbstractSideProofRule.createResultConstant(Services services,
Sort sort)
Creates a constant which is used in the original
Proof to
store the computed result in form of QueryResult = ... |
protected Function |
AbstractSideProofRule.createResultFunction(Services services,
Sort sort)
Creates the result
Function used in a predicate to compute the result in the side proof. |
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 |
---|---|
void |
UserDefinedSymbols.addFunction(Function symbol) |
void |
UserDefinedSymbols.addPredicate(Function symbol) |
Modifier and Type | Method and Description |
---|---|
static Function |
MergeRuleUtils.getNewSkolemConstantForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a new Skolem constant with the given prefix in its
name of the given sort.
|
Modifier and Type | Method and Description |
---|---|
static java.util.HashSet<Function> |
MergeRuleUtils.getSkolemConstants(Term term)
Returns all Skolem constants in the given term.
|
Modifier and Type | Method and Description |
---|---|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term by fresh variables.
|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashSet<Function> restrictTo,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term that are contained in the set
restrictTo by fresh variables.
|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashSet<Function> restrictTo,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term that are contained in the set
restrictTo by fresh variables.
|
Copyright © 2003-2019 The KeY-Project.