Packages

package root

KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics.

KeYmaera X: An aXiomatic Tactical Theorem Prover

KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.

http://keymaeraX.org/

Concrete syntax for input language Differential Dynamic Logic

Package Structure

Main documentation entry points for KeYmaera X API:

edu.cmu.cs.ls.keymaerax.core - KeYmaera X kernel, proof certificates, main data structures
- Expression - Differential dynamic logic expressions: Term, Formula, Program
- Sequent - Sequents of formulas
- Provable - Proof certificates transformed by rules/axioms
- Rule - Proof rules as well as USubstOne for (one-pass) uniform substitutions and renaming.
- StaticSemantics - Static semantics with free and bound variable analysis
- Instead of constructing dL expressions from constructors, it is easier to use the KeYmaeraXParser.
edu.cmu.cs.ls.keymaerax.parser - Parser and pretty printer with concrete syntax and notation for differential dynamic logic.
- Concrete syntax for input language Differential Dynamic Logic
- KeYmaeraXPrettyPrinter - Pretty printer producing concrete KeYmaera X syntax
- KeYmaeraXParser - Parser reading concrete KeYmaera X syntax
- KeYmaeraXArchiveParser - Parser reading KeYmaera X model and proof archive .kyx files
- DLParser - Combinator parser reading concrete KeYmaera X syntax
- DLArchiveParser - Combinator parser reading KeYmaera X model and proof archive .kyx files
edu.cmu.cs.ls.keymaerax.infrastruct - Prover infrastructure outside the kernel
- UnificationMatch - Unification algorithm
- RenUSubst - Renaming Uniform Substitution quickly combining kernel's renaming and substitution.
- Context - Representation for contexts of formulas in which they occur.
- Augmentors - Augmenting formula and expression data structures with additional functionality
- ExpressionTraversal - Generic traversal functionality for expressions
edu.cmu.cs.ls.keymaerax.bellerophon - Bellerophon tactic language and tactic interpreter
- BelleExpr - Tactic language expressions
- SequentialInterpreter - Sequential tactic interpreter for Bellerophon tactics
edu.cmu.cs.ls.keymaerax.btactics - Bellerophon tactic library for conducting proofs.
- TactixLibrary - Main KeYmaera X tactic library including many proof tactics.
- HilbertCalculus - Hilbert Calculus for differential dynamic logic
- SequentCalculus - Sequent Calculus for propositional and first-order logic
- HybridProgramCalculus - Hybrid Program Calculus for differential dynamic logic
- DifferentialEquationCalculus - Differential Equation Calculus for differential dynamic logic
- UnifyUSCalculus - Unification-based uniform substitution calculus underlying the other calculi
- [edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic] - Forward tactic framework for conducting proofs from premises to conclusions
edu.cmu.cs.ls.keymaerax.lemma - Lemma mechanism
- Lemma - Lemmas are Provables stored under a name, e.g., in files.
- LemmaDB - Lemma database stored in files or database etc.
edu.cmu.cs.ls.keymaerax.tools.qe - Real arithmetic back-end solvers
- MathematicaQETool - Mathematica interface for real arithmetic.
- Z3QETool - Z3 interface for real arithmetic.
edu.cmu.cs.ls.keymaerax.tools.ext - Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.
- Mathematica - Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.
- Z3 - Z3 interface for real arithmetic including simplifiers.

Entry Points

Additional entry points and usage points for KeYmaera X API:

edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX - Command-line launcher for KeYmaera X supports command-line argument -help to obtain usage information
edu.cmu.cs.ls.keymaerax.btactics.AxIndex - Axiom indexing data structures with keys and recursors for canonical proof strategies.
edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo - Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.
edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex - Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.
edu.cmu.cs.ls.keymaerax.btactics.Ax - Registry for derived axioms and axiomatic proof rules that are proved from the core.

References

Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:

1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.

2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.

3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos

Definition Classes: root

package edu

Definition Classes: root

package cmu

Definition Classes: edu

package cs

Definition Classes: cmu

package ls

Definition Classes: cs

package keymaerax

Definition Classes: ls

package parser

Parser & Pretty-Printer for Differential Dynamic Logic

Defines the concrete syntax of differential dynamic logic as used in KeYmaera X. Provides a parser to read string and file inputs with differential dynamic logic. Conversely provides a pretty-printer to format differential dynamic logic expression data structure as human readable concrete syntax.

PrettyPrinter: Expression => String
Parser: String => Expression

Usage Overview

The default pretty-printer for the concrete syntax in KeYmaera X is in edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter. The corresponding parser for the concrete syntax in edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser. Also see Grammar of KeYmaera X Syntax

val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
println("Printed:  " + print)

Printing Differential Dynamic Logic

edu.cmu.cs.ls.keymaerax.parser.PrettyPrinter defines the interface for all differential dynamic logic pretty printers in KeYmaera X.

PrettyPrinter: Expression => String

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter implements the pretty-printer for the concrete syntax of differential dynamic logic used in KeYmaera X. A pretty-printer is an injective function from differential dynamic logic expressions to strings.

Printing formulas to strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter.apply:

val pp = KeYmaeraXPrettyPrinter
// "x < -y"
val fml0 = Less(Variable("x"),Neg(Variable("y")))
val fml0str = pp(fml0)
// "true -> [x:=1;]x>=0"
val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
val fml1str = pp(fml1)

Printing Fully Parenthesized Forms

Fully parenthesized strings are obtained using the edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter printer:

val pp = FullPrettyPrinter
// "x < -(y)"
val fml0 = Less(Variable("x"),Neg(Variable("y")))
val fml0str = pp(fml0)
// "true -> ([x:=1;](x>=0))"
val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
val fml1str = pp(fml1)

The fully-parenthesized pretty printer corresponding to a pretty printer can also be obtained using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrinter.fullPrinter

Parsing Differential Dynamic Logic

edu.cmu.cs.ls.keymaerax.parser.Parser defines the interface for all differential dynamic logic parsers in KeYmaera X.

Parser: String => Expression

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser implements the parser for the concrete syntax of differential dynamic logic used in KeYmaera X. A parser is a function from input strings to differential dynamic logic expressions.

Parsing formulas from strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply:

val parser = KeYmaeraXParser
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")

The parser parses any dL expression, so will also accept terms or programs from strings, which will lead to appropriate types:

val parser = KeYmaeraXParser
// formulas
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
// terms
val term0 = parser("x+5")
val term1 = parser("x^2-2*x+7")
val term2 = parser("x*y/3+(x-1)^2+5*z")
// programs
val prog0 = parser("x:=1;")
val prog1 = parser("x:=1;x:=5;x:=-1;")
val prog2 = parser("x:=1;{{x'=5}++x:=0;}")

Parsing Only Formulas of Differential Dynamic Logic

The parser that only parses formulas is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.formulaParser

// the formula parser only accepts formulas
val parser = KeYmaeraXParser.formulaParser
// formulas
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
// terms will cause exceptions
try { parser("x+5") } catch {case e: ParseException => println("Rejected")}
// programs will cause exceptions
try { parser("x:=1;") } catch {case e: ParseException => println("Rejected")}

Similarly, a parser that only parses terms is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.termParser and a parser that only parses programs is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.programParser

Parsing Pretty-Printed Strings

Corresponding parsers and pretty-printers match with one another. Parsing a pretty-printed expression results in the original expression again:

parse(print(e)) == e

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser and are inverses in this sense. The converse print(parse(s)) == s is not quite the case, because there can be minor spacing and superfluous parentheses differences. The following slightly weaker form still holds:

parse(print(parse(s))) == parse(s)

Parsing the pretty-print of an expression with compatible printers and parsers always gives the original expression back:

val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val fml = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
// something like "true -> [x:=1;]x>=0" modulo spacing
val print = pp(fml)
val reparse = parser(print)
if (fml == reparse) println("Print and reparse successful") else println("Discrepancy")

Pretty-Printing Parsed Strings

It can be quite helpful to print an expression that has been parsed to check how it got parsed:

val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
println("Printed:  " + print)
println("Original: " + input)
println("Can differ slightly by spacing and parentheses")

Recall that the default pretty printer uses compact parentheses and braces. That is, it only prints them when necessary to disambiguate. For storage purposes and disambiguation it can be better to use fully parenthesized printouts, which is what edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter achieves:

val parser = KeYmaeraXParser
val pp = FullPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
// (((x)^(2)>=0)&(x < 44))->([{x:=2;}{{x'=1&x<=10}}](x>=1))
println("Printed:  " + print)
println("Original: " + input)

Pretty-Printing Sequents

Sequents can be pretty-printed using the default pretty printer via edu.cmu.cs.ls.keymaerax.core.Sequent.prettyString

val parser = KeYmaeraXParser
val sequent = Sequent(IndexedSeq(parse("x<22"), parse("x>0")), IndexedSeq(parse("[x:=x+1;]x<23")))
println("Printed:  " + sequent.prettyString)

Definition Classes: keymaerax
See also: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
Grammar of Differential Dynamic Logic
edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter

ArchiveParser

AtomicBinaryFormat

AtomicFormat

AxiomFileMode

BasePrettyPrinter

BinaryNotation

BinaryOpSpec

Bottom

DLArchiveParser

DLAxiomParser

DLParser

DLParserUtils

Declaration

EOF

ExpressionMode

ExternalEvidence

FormatProvider

FullPrettyPrinter

FullPrettyPrinter0

InterpretedSymbols

KeYmaera3PrettyPrinter

KeYmaeraXArchiveParser

KeYmaeraXArchiveParserBase

KeYmaeraXArchivePrinter

KeYmaeraXAxiomParser

KeYmaeraXExtendedLemmaParser

KeYmaeraXLegacyArchivePrinter

KeYmaeraXLexer

KeYmaeraXNoContractPrettyPrinter

KeYmaeraXOmitInterpretationPrettyPrinter

KeYmaeraXParser

KeYmaeraXPrecedencePrinter

KeYmaeraXPrettierPrinter

KeYmaeraXPrettyPrinter

KeYmaeraXPrinter

KeYmaeraXSkipPrinter

KeYmaeraXStoredProvableParser

KeYmaeraXWeightedPrettyPrinter

LeftAssociative

LemmaFileMode

LexException

LexerMode

Location

MixedBinary

Name

NonAssociative

NoneFormatProvider

NullaryNotation

ODEToInterpreted

OpNotation

OpSpec

ParseException

ParsedArchiveEntry

Parser

ParserHelper

ParserInit

PostfixFormat

PrefixFormat

PrettierPrintFormatProvider

PrettyPrintFormatProvider

PrettyPrinter

ProblemFileMode

ProofEvidence

Region

ReservedSymbols

RightAssociative

SequentParser

Signature

Stack

StoredProvableMode

StringConverter

SubstitutionParser

SuffixRegion

TacticReservedSymbols

Terminal

TernaryNotation

TernaryOpSpec

TernaryPrefixFormat

TokenParser

UnaryNotation

UnaryOpSpec

UnificationSubstitutionParser

UnitOpSpec

UnknownLocation

edu.cmu.cs.ls.keymaerax.parser

DLParser

Companion class DLParser

object DLParser extends DLParser

Differential Dynamic Logic parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.

See also: KeYmaeraXParser

Linear Supertypes

DLParser, Parser, (String) ⇒ Expression, AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

DLParser
DLParser
Parser
Function1
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def ambiguousBaseF[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def andThen[A](g: (Expression) ⇒ A): (String) ⇒ A

Definition Classes
Function1
Annotations
@unspecialized()
def annotation[_](implicit arg0: P[Any]): P[Seq[Formula]]
Parses an annotation
Parses an annotation

Definition Classes
DLParser
def annotationListener: (Program, Formula) ⇒ Unit
Returns the annotation listener.
Returns the annotation listener.

Definition Classes
DLParser → Parser
def apply(input: String): Expression
Parse the input string in the concrete syntax as a differential dynamic logic expression
Parse the input string in the concrete syntax as a differential dynamic logic expression
input
the string to parse as a dL formula, dL term, or dL program.

Definition Classes
DLParser → Parser → Function1
Exceptions thrown
ParseException if input is not a well-formed expression of differential dynamic logic or differential game logic.
final def asInstanceOf[T0]: T0

Definition Classes
Any
def assign[_](implicit arg0: P[Any]): P[AtomicProgram]

Definition Classes
DLParser
def atomicDP[_](implicit arg0: P[Any]): P[AtomicDifferentialProgram]

Definition Classes
DLParser
def backImplication[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def baseF[_](implicit arg0: P[Any]): P[Formula]
Base formulas
Base formulas

Definition Classes
DLParser
def baseP[_](implicit arg0: P[Any]): P[Program]

Definition Classes
DLParser
def baseTerm[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Term]

Definition Classes
DLParser
def baseVariable[_](implicit arg0: P[Any]): P[BaseVariable]

Definition Classes
DLParser
def biimplication[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def blank[_](implicit arg0: P[Any]): P[Unit]
Explicit nonempty whitespace terminal.
Explicit nonempty whitespace terminal.

Definition Classes
DLParser
def braceP[_](implicit arg0: P[Any]): P[Program]

Definition Classes
DLParser
def choice[_](implicit arg0: P[Any]): P[Program]

Definition Classes
DLParser
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
def comparator[_](implicit arg0: P[Any]): P[Unit]

Definition Classes
DLParser
def comparison[_](implicit arg0: P[Any]): P[Formula]
Parses a comparison, given the left-hand term
Parses a comparison, given the left-hand term

Definition Classes
DLParser
def compose[A](g: (A) ⇒ String): (A) ⇒ Expression

Definition Classes
Function1
Annotations
@unspecialized()
def conjunct[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def diff[_](left: Term)(implicit arg0: P[Any]): P[Term]
Parses term'
Parses term'

Definition Classes
DLParser
def diffExercise[_](implicit arg0: P[Any]): P[DifferentialProgramConst]

Definition Classes
DLParser
def diffProduct[_](implicit arg0: P[Any]): P[DifferentialProgram]

Definition Classes
DLParser
def diffProgram[_](implicit arg0: P[Any]): P[DifferentialProgram]
diffProgram: Parses a dL differential program.
diffProgram: Parses a dL differential program.

Definition Classes
DLParser
def diffProgramSymbol[_](implicit arg0: P[Any]): P[DifferentialProgramConst]

Definition Classes
DLParser
def diffVariable[_](implicit arg0: P[Any]): P[DifferentialSymbol]

Definition Classes
DLParser
val differentialProgramParser: (String) ⇒ DifferentialProgram
Parse the input string in the concrete syntax as a differential dynamic logic differential program
Parse the input string in the concrete syntax as a differential dynamic logic differential program

Definition Classes
DLParser → Parser
def disjunct[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def dot[_](implicit arg0: P[Any]): P[DotTerm]
. or ._2: dot parsing
. or ._2: dot parsing

Definition Classes
DLParser
def dual[_](implicit arg0: P[Any]): P[Program]
Parses dual notation: baseP or baseP^@
Parses dual notation: baseP or baseP^@

Definition Classes
DLParser
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
val exprParser: (String) ⇒ Expression
Parse the input string in the concrete syntax as a differential dynamic logic expression
Parse the input string in the concrete syntax as a differential dynamic logic expression

Definition Classes
DLParser
def expression[_](implicit arg0: P[Any]): P[Expression]

Definition Classes
DLParser
def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
def formula[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
val formulaParser: (String) ⇒ Formula
Parse the input string in the concrete syntax as a differential dynamic logic formula
Parse the input string in the concrete syntax as a differential dynamic logic formula

Definition Classes
DLParser → Parser
def fullDifferentialProgram[_](implicit arg0: P[Any]): P[DifferentialProgram]

Definition Classes
DLParser
def fullExpression[_](implicit arg0: P[Any]): P[Expression]

Definition Classes
DLParser
def fullFormula[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def fullProgram[_](implicit arg0: P[Any]): P[Program]

Definition Classes
DLParser
def fullSequent[_](implicit arg0: P[Any]): P[Sequent]

Definition Classes
DLParser
def fullSequentList[_](implicit arg0: P[Any]): P[List[Sequent]]

Definition Classes
DLParser
def fullTerm[_](implicit arg0: P[Any]): P[Term]

Definition Classes
DLParser
def function[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[FuncOf]

Definition Classes
DLParser
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@native()
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@native()
def ident[_](implicit arg0: P[Any]): P[(String, Option[Int])]
parse an identifier.
parse an identifier.
returns
the name and its index (if any).

Definition Classes
DLParser
Note
Index is normalized so that x_00 cannot be mentioned and confused with x_0.
,
Keywords are not allowed as identifiers.
def ifthen[_](implicit arg0: P[Any]): P[Program]

Definition Classes
DLParser
def implication[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def integer[_](implicit arg0: P[Any]): P[Int]
"-532": Parse an integer literal, unnormalized.
"-532": Parse an integer literal, unnormalized.

Definition Classes
DLParser
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
def keywords: Set[String]
matches keywords.
matches keywords. An identifier cannot be a keyword.

Definition Classes
DLParser
def multiplicand[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Term]

Definition Classes
DLParser
def natural[_](implicit arg0: P[Any]): P[Int]
"532": Parse a (nonnegative) natural number literal, unnormalized.
"532": Parse a (nonnegative) natural number literal, unnormalized.

Definition Classes
DLParser
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def negNumberLiteral[_](implicit arg0: P[Any]): P[Number]
parse a number literal enclosed in (), which is allowed to be a negative number
parse a number literal enclosed in (), which is allowed to be a negative number

Definition Classes
DLParser
def normNatural[_](implicit arg0: P[Any]): P[Int]
"532": Parse a (nonnegative) natural number literal, normalized.
"532": Parse a (nonnegative) natural number literal, normalized.

Definition Classes
DLParser
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@native()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@native()
def number[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Number]
parses a number
parses a number

Definition Classes
DLParser
def numberLiteral[_](implicit arg0: P[Any]): P[Number]
parses a number literal
parses a number literal

Definition Classes
DLParser
def ode[_](implicit arg0: P[Any]): P[AtomicODE]

Definition Classes
DLParser
def odeSpace[_](implicit arg0: P[Any]): P[Space]
{|x1,x2,x3|} parses a space declaration
{|x1,x2,x3|} parses a space declaration

Definition Classes
DLParser
def odeprogram[_](implicit arg0: P[Any]): P[ODESystem]

Definition Classes
DLParser
def odesystem[_](implicit arg0: P[Any]): P[ODESystem]

Definition Classes
DLParser
def predicational[_](implicit arg0: P[Any]): P[PredicationalOf]
Regular predicationals C{}
Regular predicationals C{}

Definition Classes
DLParser
lazy val printer: KeYmaeraXPrettyPrinter.type
A pretty-printer that can write the output that this parser reads
A pretty-printer that can write the output that this parser reads

Definition Classes
DLParser → Parser
def program[_](implicit arg0: P[Any]): P[Program]
program: Parses a dL program.
program: Parses a dL program.

Definition Classes
DLParser
def programExercise[_](implicit arg0: P[Any]): P[AtomicProgram]

Definition Classes
DLParser
val programParser: (String) ⇒ Program
Parse the input string in the concrete syntax as a differential dynamic logic program
Parse the input string in the concrete syntax as a differential dynamic logic program

Definition Classes
DLParser → Parser
def programSymbol[_](implicit arg0: P[Any]): P[AtomicProgram]

Definition Classes
DLParser
def sequence[_](implicit arg0: P[Any]): P[Program]

Definition Classes
DLParser
def sequent[_](implicit arg0: P[Any]): P[Sequent]
sequent ::= aformula1 , aformula2 , ... , aformulan ==> sformula1 , sformula2 , ... , sformulam.
sequent ::= aformula1 , aformula2 , ... , aformulan ==> sformula1 , sformula2 , ... , sformulam.

Definition Classes
DLParser
def sequentList[_](implicit arg0: P[Any]): P[List[Sequent]]
sequentList ::= sequent ;; sequent ;; ...
sequentList ::= sequent ;; sequent ;; ... ;; sequent.

Definition Classes
DLParser
val sequentParser: (String) ⇒ Sequent
Parse the input string in the concrete syntax as a differential dynamic logic sequent.
Parse the input string in the concrete syntax as a differential dynamic logic sequent.

Definition Classes
DLParser → Parser
def setAnnotationListener(listener: (Program, Formula) ⇒ Unit): Unit
Register a listener for @annotations during the parse.
Register a listener for @annotations during the parse.

Definition Classes
DLParser → Parser
To do
this design is suboptimal.
def signed[_](p: ⇒ P[Term])(implicit arg0: P[Any]): P[Either[Term, Term]]
p | -p: possibly signed occurrences of what is parsed by parser p Note we try p before -p because some parsers (like number) also consume -s.
p | -p: possibly signed occurrences of what is parsed by parser p Note we try p before -p because some parsers (like number) also consume -s. Distinguishes between Left(Neg(x)) = (-x) and Right(Neg(x)) = -x.

Definition Classes
DLParser
def space[_](implicit arg0: P[Any]): P[Space]
(|x1,x2,x3|) parses a space declaration
(|x1,x2,x3|) parses a space declaration

Definition Classes
DLParser
def string[_](implicit arg0: P[Any]): P[String]
"whatevs": Parse a string literal.
"whatevs": Parse a string literal. (([^\\"]|\\"|\\(?!"))*+)

Definition Classes
DLParser
def stringInterior[_](implicit arg0: P[Any]): P[String]

Definition Classes
DLParser
def summand[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Term]

Definition Classes
DLParser
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def systemSymbol[_](implicit arg0: P[Any]): P[AtomicProgram]

Definition Classes
DLParser
def term[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Term]
Parse a term.
Parse a term.
Some terms are ambiguous with formulas, in particular
- Parentheses (term parens vs function parens)
- Functions vs predicates
- UnitFunctionals vs UnitPredicationals So, we want to allow backtracking on these ambiguous syntax forms if we are not sure whether the input is a term or a formula.
If doAmbigCuts is true, we assume the input is a term, and perform all permissible cuts. If it is false, we only perform cuts that are unambiguous indicators the input is a term.
Definition Classes
DLParser
def termList[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[Term]
(t1,t2,t3,...,tn) parenthesized list of terms
(t1,t2,t3,...,tn) parenthesized list of terms

Definition Classes
DLParser
val termParser: (String) ⇒ Term
Parse the input string in the concrete syntax as a differential dynamic logic term
Parse the input string in the concrete syntax as a differential dynamic logic term

Definition Classes
DLParser → Parser
def test[_](implicit arg0: P[Any]): P[Test]

Definition Classes
DLParser
def toString(): String

Definition Classes
Function1 → AnyRef → Any
def unambiguousBaseF[_](implicit arg0: P[Any]): P[Formula]

Definition Classes
DLParser
def unitFunctional[_](doAmbigCuts: Boolean)(implicit arg0: P[Any]): P[UnitFunctional]

Definition Classes
DLParser
def unitPredicational[_](implicit arg0: P[Any]): P[UnitPredicational]
Unit predicationals c(||)
Unit predicationals c(||)

Definition Classes
DLParser
def variable[_](implicit arg0: P[Any]): P[Variable]

Definition Classes
DLParser
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@native() @throws( ... )

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Usage Overview

Printing Differential Dynamic Logic

Printing Fully Parenthesized Forms

Parsing Differential Dynamic Logic

Parsing Only Formulas of Differential Dynamic Logic

Parsing Pretty-Printed Strings

Pretty-Printing Parsed Strings

Pretty-Printing Sequents

DLParser

Companion class DLParser

object DLParser extends DLParser

Value Members

Inherited from DLParser

Inherited from Parser

Inherited from (String) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Usage Overview

Printing Differential Dynamic Logic

Printing Fully Parenthesized Forms

Parsing Differential Dynamic Logic

Parsing Only Formulas of Differential Dynamic Logic

Parsing Pretty-Printed Strings

Pretty-Printing Parsed Strings

Pretty-Printing Sequents

DLParser 

Companion class DLParser

object DLParser extends DLParser

Value Members

Inherited from DLParser

Inherited from Parser

Inherited from (String) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped

DLParser