Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
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.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 |
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.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
static java.util.List<AbstractionPredicate> |
AbstractionPredicate.fromString(java.lang.String s,
Services services,
NamespaceSet localNamespaces)
Parses the String representation of an abstraction predicates.
|
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
TacletFindModel(TacletApp app,
Services services,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for tree.
|
TacletInstantiationModel(TacletApp app,
Sequent seq,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for the apply Taclet dialog wrapping a combo box model
and a table model.
|
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
KeYMediator.namespaces()
returns the namespace set
|
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
Services.getNamespaces()
returns the namespaces for functions, predicates etc.
|
Modifier and Type | Method and Description |
---|---|
Services |
Services.getOverlay(NamespaceSet namespaces) |
protected Recoder2KeYConverter |
Recoder2KeY.makeConverter(Services services,
NamespaceSet nss)
create the ast converter.
|
protected Recoder2KeYConverter |
SchemaRecoder2KeY.makeConverter(Services services,
NamespaceSet nss) |
JavaBlock |
KeYProgModelInfo.readBlock(java.lang.String block,
ClassDeclaration cd,
NamespaceSet nss)
Parses a given JavaBlock using cd as context to determine the right
references.
|
JavaBlock |
KeYProgModelInfo.readJavaBlock(java.lang.String block,
NamespaceSet nss)
Parses a given JavaBlock using an empty context.
|
void |
Services.setNamespaces(NamespaceSet namespaces)
sets the namespaces of known predicates, functions, variables
|
Constructor and Description |
---|
Recoder2KeY(Services services,
KeYCrossReferenceServiceConfiguration servConf,
KeYRecoderMapping rec2key,
NamespaceSet nss,
TypeConverter tc)
create a new Recoder2KeY transformation object.
|
Recoder2KeY(Services services,
NamespaceSet nss)
create a new Recoder2KeY transformation object.
|
Recoder2KeYConverter(Recoder2KeY rec2key,
Services services,
NamespaceSet nss) |
Recoder2KeYTypeConverter(Services services,
TypeConverter typeConverter,
NamespaceSet namespaces,
Recoder2KeY recoder2key) |
SchemaRecoder2KeY(Services services,
NamespaceSet nss) |
SchemaRecoder2KeYConverter(SchemaRecoder2KeY rec2key,
Services services,
NamespaceSet namespaceSet)
create a new schema-recoder-to-key converter.
|
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
NamespaceSet.copy() |
NamespaceSet |
NamespaceSet.copyWithParent() |
NamespaceSet |
NamespaceSet.getCompression() |
NamespaceSet |
TermServices.getNamespaces()
returns the namespaces for functions, predicates etc.
|
NamespaceSet |
NamespaceSet.getParent() |
NamespaceSet |
NamespaceSet.shallowCopy() |
NamespaceSet |
NamespaceSet.simplify() |
Modifier and Type | Method and Description |
---|---|
void |
NamespaceSet.add(NamespaceSet ns) |
java.lang.String |
TermBuilder.newName(java.lang.String baseName,
NamespaceSet localNamespace)
Returns an available name constructed by affixing a counter to the passed
base name.
|
Term |
TermBuilder.parseTerm(java.lang.String s,
NamespaceSet namespaces)
Parses the given string that represents the term (or createTerm) using
the provided namespaces.
|
Constructor and Description |
---|
KeyIO(Services services,
NamespaceSet nss) |
Modifier and Type | Field and Description |
---|---|
protected NamespaceSet |
DefaultBuilder.nss |
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
DefaultBuilder.namespaces() |
Constructor and Description |
---|
ContractsAndInvariantsFinder(Services services,
NamespaceSet nss) |
DeclarationBuilder(Services services,
NamespaceSet nss) |
DefaultBuilder(Services services,
NamespaceSet nss) |
ExpressionBuilder(Services services,
NamespaceSet nss) |
ExpressionBuilder(Services services,
NamespaceSet nss,
Namespace<SchemaVariable> schemaNamespace) |
FunctionPredicateBuilder(Services services,
NamespaceSet nss) |
ProblemFinder(Services services,
NamespaceSet nss) |
TacletPBuilder(Services services,
NamespaceSet nss) |
TacletPBuilder(Services services,
NamespaceSet namespaces,
java.util.HashMap<Taclet,TacletBuilder<? extends Taclet>> taclet2Builder) |
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
ParserConfig.namespaces() |
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
NamespaceSet nss,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Sequent |
DefaultTermParser.parseSeq(java.io.Reader in,
Services services,
NamespaceSet nss,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a sequent with the
specified namespaces.
|
Constructor and Description |
---|
ParserConfig(Services services,
NamespaceSet nss) |
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
Goal.getLocalNamespaces()
returns the namespaces for this goal.
|
NamespaceSet |
Proof.getNamespaces()
returns a collection of the namespaces valid for this proof
|
Modifier and Type | Method and Description |
---|---|
void |
Goal.makeLocalNamespacesFrom(NamespaceSet ns)
Update the local namespaces from a namespace set.
|
void |
Proof.setNamespaces(NamespaceSet ns)
sets the variable, function, sort, heuristics namespaces
|
Modifier and Type | Method and Description |
---|---|
NamespaceSet |
InitConfig.namespaces()
returns the namespaces of this initial configuration
|
Modifier and Type | Method and Description |
---|---|
void |
TacletApp.registerSkolemConstants(NamespaceSet nss) |
Modifier and Type | Method and Description |
---|---|
void |
UserDefinedSymbols.addSymbolsToNamespaces(NamespaceSet namespaces) |
Constructor and Description |
---|
UserDefinedSymbols(NamespaceSet referenceNamespaces,
ImmutableSet<Taclet> axioms) |
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
MergeRuleUtils.parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
Copyright © 2003-2019 The KeY-Project.