Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
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.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.parseTerm(java.lang.String s)
Parses the given string that represents the term (or createTerm) using
the service's namespaces.
|
Term |
TermBuilder.parseTerm(java.lang.String s,
NamespaceSet namespaces)
Parses the given string that represents the term (or createTerm) using
the provided namespaces.
|
Modifier and Type | Method and Description |
---|---|
Sequent |
EngineState.toSequent(java.lang.String sequent) |
Sort |
EngineState.toSort(java.lang.String sortName) |
Term |
EngineState.toTerm(java.lang.String string,
Sort sort) |
Modifier and Type | Method and Description |
---|---|
ParserException |
ParserException.initCause(java.lang.Throwable cause) |
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,
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.
|
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.