Package | Description |
---|---|
de.uka.ilkd.key.control.instantiation_model | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.recoderext | |
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.nparser | |
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.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.settings |
Modifier and Type | Method and Description |
---|---|
Namespace<IProgramVariable> |
TacletInstantiationModel.programVariables() |
Modifier and Type | Method and Description |
---|---|
Namespace<Choice> |
KeYMediator.choice_ns()
returns the choice namespace
|
Namespace<Function> |
KeYMediator.func_ns()
returns the function namespace
|
Namespace<RuleSet> |
KeYMediator.heur_ns()
returns the heuristics namespace
|
Namespace<IProgramVariable> |
KeYMediator.progVar_ns()
returns the program variable namespace
|
Namespace<Sort> |
KeYMediator.sort_ns()
returns the sort namespace
|
Namespace<QuantifiableVariable> |
KeYMediator.var_ns()
returns the variable namespace
|
Modifier and Type | Field and Description |
---|---|
protected Namespace<SchemaVariable> |
SchemaRecoder2KeY.svns
the namespace containing the program schema variables allowed here
|
Modifier and Type | Method and Description |
---|---|
JavaBlock |
Recoder2KeY.readBlockWithProgramVariables(Namespace<IProgramVariable> varns,
java.lang.String s)
parses a given JavaBlock using a namespace to determine the right
references using an empty context.
|
JavaBlock |
JavaReader.readBlockWithProgramVariables(Namespace<IProgramVariable> varns,
java.lang.String s) |
void |
SchemaJavaReader.setSVNamespace(Namespace<SchemaVariable> ns) |
void |
SchemaRecoder2KeY.setSVNamespace(Namespace<SchemaVariable> svns) |
Modifier and Type | Field and Description |
---|---|
protected Namespace<SchemaVariable> |
SchemaJavaProgramFactory.svns |
Modifier and Type | Method and Description |
---|---|
void |
SchemaJavaProgramFactory.setSVNamespace(Namespace<SchemaVariable> ns) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<Operator> |
LDT.functions()
returns the basic functions of the model
|
Modifier and Type | Method and Description |
---|---|
Namespace<Choice> |
NamespaceSet.choices() |
Namespace<E> |
Namespace.compress() |
Namespace<E> |
Namespace.copy() |
Namespace<E> |
Namespace.extended(E sym)
creates a new Namespace that has this as parent, and contains
an entry for
sym . |
Namespace<E> |
Namespace.extended(java.lang.Iterable<? extends E> ext) |
Namespace<Function> |
NamespaceSet.functions() |
Namespace<E> |
Namespace.parent()
returns the fall-back Namespace of this Namespace, i.e.
|
Namespace<IProgramVariable> |
NamespaceSet.programVariables() |
Namespace<RuleSet> |
NamespaceSet.ruleSets() |
Namespace<E> |
Namespace.simplify() |
Namespace<Sort> |
NamespaceSet.sorts() |
Namespace<QuantifiableVariable> |
NamespaceSet.variables() |
Modifier and Type | Method and Description |
---|---|
void |
Namespace.add(Namespace<E> source) |
void |
NamespaceSet.setChoices(Namespace<Choice> choiceNS) |
void |
NamespaceSet.setFunctions(Namespace<Function> funcNS) |
void |
NamespaceSet.setProgramVariables(Namespace<IProgramVariable> progVarNS) |
void |
NamespaceSet.setRuleSets(Namespace<RuleSet> ruleSetNS) |
void |
NamespaceSet.setSorts(Namespace<Sort> sortNS) |
void |
NamespaceSet.setVariables(Namespace<QuantifiableVariable> varNS) |
Modifier and Type | Method and Description |
---|---|
Namespace<Choice> |
ChoiceInformation.getChoices() |
Namespace<SchemaVariable> |
KeyIO.Loader.getSchemaNamespace() |
Modifier and Type | Method and Description |
---|---|
void |
KeyIO.setSchemaNamespace(Namespace<SchemaVariable> ns) |
Constructor and Description |
---|
ChoiceInformation(Namespace<Choice> choices) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<Choice> |
DefaultBuilder.choices() |
protected Namespace<Function> |
DefaultBuilder.functions() |
protected Namespace<IProgramVariable> |
DefaultBuilder.programVariables() |
protected Namespace<RuleSet> |
DefaultBuilder.ruleSets() |
Namespace<SchemaVariable> |
DefaultBuilder.schemaVariables() |
protected Namespace<Sort> |
DefaultBuilder.sorts() |
protected Namespace<QuantifiableVariable> |
DefaultBuilder.variables() |
Modifier and Type | Method and Description |
---|---|
protected <T> T |
DefaultBuilder.doLookup(Name n,
Namespace... lookups) |
void |
DefaultBuilder.setSchemaVariables(Namespace<SchemaVariable> ns) |
protected void |
DefaultBuilder.unbindVars(Namespace<QuantifiableVariable> orig) |
Constructor and Description |
---|
ChoiceFinder(Namespace<Choice> choices) |
ExpressionBuilder(Services services,
NamespaceSet nss,
Namespace<SchemaVariable> schemaNamespace) |
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.
|
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.
|
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.
|
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.
|
Modifier and Type | Method and Description |
---|---|
Namespace<Choice> |
InitConfig.choiceNS()
returns the choice namespace of this initial configuration
|
Namespace<Function> |
InitConfig.funcNS()
returns the function namespace of this initial configuration.
|
Namespace<IProgramVariable> |
InitConfig.progVarNS()
returns the program variable namespace of this initial configuration
|
Namespace<RuleSet> |
InitConfig.ruleSetNS()
returns the heuristics namespace of this initial configuration
|
Namespace<Sort> |
InitConfig.sortNS()
returns the sort namespace of this initial configuration
|
Namespace<QuantifiableVariable> |
InitConfig.varNS()
returns the variable namespace of this initial configuration
|
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.
|
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.
|
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 |
---|---|
Namespace<Function> |
TacletApp.extendedFunctionNameSpace(Namespace<Function> func_ns)
create a new function namespace by adding all newly instantiated skolem
symbols to a new namespace.
|
Namespace<QuantifiableVariable> |
TacletApp.extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns,
SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations of
the schema variables in the context of the given schema variable and (if
the TacletApp's prefix has the context flag set) by adding names of the
logic variables of the context.
|
Modifier and Type | Method and Description |
---|---|
Namespace<Function> |
TacletApp.extendedFunctionNameSpace(Namespace<Function> func_ns)
create a new function namespace by adding all newly instantiated skolem
symbols to a new namespace.
|
Namespace<QuantifiableVariable> |
TacletApp.extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns,
SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations of
the schema variables in the context of the given schema variable and (if
the TacletApp's prefix has the context flag set) by adding names of the
logic variables of the context.
|
Modifier and Type | Method and Description |
---|---|
void |
ChoiceSettings.updateChoices(Namespace<Choice> choiceNS,
boolean remove)
updates
category2Choices if new entries are found
in choiceNS or if entries of category2Choices
are no longer present in choiceNS |
Copyright © 2003-2019 The KeY-Project.