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)
- 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.
- Alphabetic
- By Inheritance
- parser
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
:+[A](tail: Stack[A], top: A) extends Stack[A] with Product with Serializable
A stack tail :+ top with top on the top of tail
- trait ArchiveParser extends (String) ⇒ List[ParsedArchiveEntry]
-
trait
BasePrettyPrinter extends PrettyPrinter
Common base functionality for KeYmaera X Pretty Printers.
-
trait
BinaryNotation extends OpNotation
Notational specification for binary operators of arity 2
-
case class
BinaryOpSpec[T <: Expression](op: Terminal, prec: Int, assoc: BinaryNotation, kind: (Kind, Kind), const: (String, T, T) ⇒ T) extends OpSpec with Product with Serializable
Binary operator notation specification with a constructor and expected argument kinds.
-
class
DLArchiveParser extends ArchiveParser
Parse a differential dynamic logic archive file string to a list of archive entries.
Parse a differential dynamic logic archive file string to a list of archive entries. Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers. An archive contains at least one entry combining a model in the
.kyxformat and possibly a (partial) proof tactic.Format example:
ArchiveEntry "Entry 1". Description "optional description text". ProgramVariables ... End. Definitions ... End. Problem ... End. Tactic "Proof 1" ... End. Tactic "Proof 2" ... End. End. ArchiveEntry "Entry 2". ... End.
- See also
-
class
DLParser extends Parser
Differential Dynamic Logic parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.
Differential Dynamic Logic parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.
Parsing formulas from strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply:
val parser = DLParser val fml0 = parser("x!=5") val fml1 = parser("x>0 -> [x:=x+1;]x>1") val fml2 = parser("x>=0 -> [{x'=2}]x>=0") // parse only formulas val fml3 = parser.formulaParser("x>=0 -> [{x'=2}]x>=0") // parse only programs/games val prog1 = parser.programParser("x:=x+1;{x'=2}") // parse only terms val term1 = parser.termParser("x^2+2*x+1")
- See also
Example: -
case class
Declaration(decls: Map[Name, Signature]) extends Product with Serializable
A parsed declaration, which assigns a signature to names.
A parsed declaration, which assigns a signature to names. This is the central data structure remembering which name belongs to which function/predicate/program symbol declaration of a model in an archive.
- case class ExternalEvidence() extends Evidence with Product with Serializable
- trait FormatProvider extends AnyRef
-
abstract
class
KeYmaeraXArchiveParserBase extends ArchiveParser
Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers.
Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers. An archive contains at least one entry combining a model in the
.kyxformat and possibly a (partial) proof tactic.Format example:
ArchiveEntry "Entry 1". Description "optional description text". ProgramVariables ... End. Definitions ... End. Problem ... End. Tactic "Proof 1" ... End. Tactic "Proof 2" ... End. End. ArchiveEntry "Entry 2". ... End.
- See also
-
class
KeYmaeraXArchivePrinter extends (ParsedArchiveEntry) ⇒ String
Prints a KeYmaera X archive.
Prints a KeYmaera X archive.
Format example:
ArchiveEntry "Entry 1". Functions. ... End. ProgramVariables. ... End. Problem. ... End. Tactic "Proof 1". ... End. Tactic "Proof 2". ... End. End. Lemma "Entry 2". ... End.
Created by smitsch on 01/04/18.
- class KeYmaeraXLegacyArchivePrinter extends (ParsedArchiveEntry) ⇒ String
-
class
KeYmaeraXOmitInterpretationPrettyPrinter extends KeYmaeraXPrecedencePrinter
A pretty printer that omits the interpretations of interpreted functions.
-
class
KeYmaeraXParser extends Parser with TokenParser with Logging
KeYmaera X parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.
KeYmaera X parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.
Also consider using the alternative parser DLParser.
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") // parse only formulas val fml3 = parser.formulaParser("x>=0 -> [{x'=2}]x>=0") // parse only programs/games val prog1 = parser.programParser("x:=x+1;{x'=2}") // parse only terms val term1 = parser.termParser("x^2+2*x+1")
- See also
Example: -
class
KeYmaeraXPrecedencePrinter extends KeYmaeraXSkipPrinter
Precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end
;Precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end
;- To do
Augment with ensures postconditions that check correct reparse non-recursively.
- See also
-
class
KeYmaeraXPrettierPrinter extends KeYmaeraXPrecedencePrinter
Vertical layout using an implementation based on Wadler's "A Prettier Printer"
Vertical layout using an implementation based on Wadler's "A Prettier Printer"
-
class
KeYmaeraXPrinter extends BasePrettyPrinter
Vanilla: KeYmaera X Printer formats differential dynamic logic expressions in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end
;Vanilla: KeYmaera X Printer formats differential dynamic logic expressions in KeYmaera X notation according to the concrete syntax of differential dynamic logic with explicit statement end
;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)
- See also
Example: -
abstract
class
KeYmaeraXSkipPrinter extends KeYmaeraXPrinter
KeYmaera X Printer base class formatting based on parentheses skipping decisions.
-
sealed abstract
class
LexerMode extends AnyRef
LexerModes corresponds to file types.
-
sealed
trait
Location extends Serializable
The location where a Terminal is located in an input stream.
The location where a Terminal is located in an input stream.
- Note
Serializable to make sure sbt test allows Location in ParseException errors.
-
case class
Name(name: String, index: Option[Int] = None) extends Product with Serializable
Name is alphanumeric name and index.
-
class
NoneFormatProvider extends FormatProvider
Noop format provider.
-
trait
NullaryNotation extends OpNotation
Notational specification for nullary operators of arity 0
-
sealed
trait
OpNotation extends AnyRef
Operator associativity notational specification
-
trait
OpSpec extends Ordered[OpSpec]
Operator notation specification with precedence and associativity.
Operator notation specification with precedence and associativity.
- To do
Could add spacing weight information to determine how much spacing is added around an operator. Alternatively, spacing weight can be inferred from the prec numerics and how far they are apart.
-
case class
ParseException(msg: String, loc: Location, found: String, expect: String, after: String, state: String, cause: Throwable = null, hint: String = "") extends ProverException with Product with Serializable
Indicates a parse error at the given location, with the context information state.
Indicates a parse error at the given location, with the context information state.
- See also
ProverException.getContext
-
case class
ParsedArchiveEntry(name: String, kind: String, fileContent: String, problemContent: String, defs: Declaration, model: Expression, tactics: List[(String, String, BelleExpr)], annotations: List[(Expression, Expression)], info: Map[String, String]) extends Product with Serializable
The entry name, kyx file content (model), definitions, parsed model, and parsed named tactics.
-
trait
Parser extends (String) ⇒ Expression
Parser interface for KeYmaera X.
Parser interface for KeYmaera X. Provides a parser to read string inputs as differential dynamic logic. A parser is a function from input strings to differential dynamic logic expressions.
Parser: String => Expression
Parsers are adjoint to printers, i.e., they reparse printed expressions as the original expressions but fail to parse syntactically ill-formed strings:
parser(printer(expr)) == expr
- See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
-
case class
PrettierPrintFormatProvider(e: Expression, margin: Int) extends PrettyPrintFormatProvider with Product with Serializable
Uses the KeYmaeraXPrettierPrinter to provide formatting for expression
efitting intomargin. -
abstract
class
PrettyPrintFormatProvider extends FormatProvider
Stateful format provider to read off whitespace and line breaks from a pretty-printed string.
-
trait
PrettyPrinter extends (Expression) ⇒ String
Pretty-Printer interface for KeYmaera X.
Pretty-Printer interface for KeYmaera X. A pretty-printer is an injective function formatting the differential dynamic logic expression data structure as human-readable concrete syntax. A pretty-printer is an injective function from differential dynamic logic expressions to strings.
PrettyPrinter: Expression => String
- See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
- case class ProofEvidence() extends Evidence with Product with Serializable
-
case class
Region(line: Int, column: Int, endLine: Int, endColumn: Int) extends Location with Product with Serializable
A region from line:column till endLine:endColumn, inclusive
-
case class
Signature(domain: Option[Sort], codomain: Sort, arguments: Option[List[(Name, Sort)]], interpretation: Option[Expression], loc: Location) extends Product with Serializable
Signature is a domain sort, codomain sort, argument names, expression used as interpretation, location that starts the declaration.
Signature is a domain sort, codomain sort, argument names, expression used as interpretation, location that starts the declaration. The signature of a function/predicate/program symbol.
- domain
the source domain required as an argument (if any).
- codomain
the resulting target domain.
- arguments
the list of named arguments (and their sorts which are compatible with
domain).- interpretation
uninterpreted symbol if None, or the interpretation of interpreted symbols.
- loc
the location in the model archive file where this was declared.
-
sealed
trait
Stack[+A] extends AnyRef
Stack with top on the right.
Stack with top on the right. For example the stack Bottom :+ a3 :+ a2 +: a1 has element a1 on the top, then a2 as the top of the tail.
-
class
StringConverter extends AnyRef
Conversions of string
sto core/tactic data structures. -
case class
SuffixRegion(line: Int, column: Int) extends Location with Product with Serializable
Like a region, but extends until the end of the input.
Like a region, but extends until the end of the input.
- line
The starting line.
- column
The ending line.
-
sealed abstract
class
Terminal extends AnyRef
Terminal symbols of the differential dynamic logic grammar.
-
trait
TernaryNotation extends OpNotation
Notational specification for ternary operators of arity 3
-
case class
TernaryOpSpec[T <: Expression](op: Terminal, op2: Terminal, op3: Terminal, prec: Int, assoc: TernaryNotation, kind: (Kind, Kind, Kind), const: (String, T, T, T) ⇒ T) extends OpSpec with Product with Serializable
Ternary operator notation specification with one terminal per operand, with constructor and expected argument kinds.
-
trait
TokenParser extends AnyRef
Parser interface for KeYmaera X reading token streams instead of strings.
Parser interface for KeYmaera X reading token streams instead of strings. Provides a parser to read token streams with differential dynamic logic. A token parser is a function from token sequences to differential dynamic logic expressions.
TokenParser: TokenStream => Expression- See also
-
trait
UnaryNotation extends OpNotation
Notational specification for unary operators of arity 1
-
case class
UnaryOpSpec[T <: Expression](op: Terminal, prec: Int, assoc: UnaryNotation, kind: Kind, const: (String, T) ⇒ T) extends OpSpec with Product with Serializable
Unary operator notation specification with a constructor and expected argument kind.
-
case class
UnitOpSpec(op: Terminal, prec: Int, const: (String) ⇒ Expression) extends OpSpec with Product with Serializable
Nullary operator notation specification with a constructor.
-
class
KeYmaeraXWeightedPrettyPrinter extends KeYmaeraXPrecedencePrinter
Weighted precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according and extra space weighted according to the concrete syntax of differential dynamic logic with explicit statement end
;Weighted precedence-based: KeYmaera X Pretty Printer formats differential dynamic logic expressions with compact brackets in KeYmaera X notation according and extra space weighted according to the concrete syntax of differential dynamic logic with explicit statement end
;- Annotations
- @deprecated
- Deprecated
Use PrettierPrinter instead
- See also
Value Members
-
final
def
checkInput(requirement: Boolean, message: ⇒ Any, loc: ⇒ Location, state: ⇒ String): Unit
Check input for requirement being true, throwing a ParseException if false.
Check input for requirement being true, throwing a ParseException if false. This method is a require coming from the parser that cannot be disabled. Blame is on the user input.
- requirement
the expression to test for being true
- message
a String explaining what is expected.
- loc
the location where the parse error occurred.
- state
information about the parser state in which the parse error occurred.
- Annotations
- @inline()
- See also
scala.Predef.require()
- object ArchiveParser extends ArchiveParser
-
object
AtomicBinaryFormat extends BinaryNotation
Atomic operators of arity 0 within syntactic category with 2 arguments from lower category
-
object
AtomicFormat extends NullaryNotation
Atomic operators of arity 0 within syntactic category
- object AxiomFileMode extends LexerMode
- object BinaryOpSpec extends Serializable
-
object
Bottom extends Stack[Nothing]
The empty stack bottom
-
object
DLAxiomParser extends (String) ⇒ List[(String, Formula)]
Parse an axiom string to a list of named formulas that are to be used as axioms in a theory.
Parse an axiom string to a list of named formulas that are to be used as axioms in a theory.
- See also
-
object
DLParser extends DLParser
Differential Dynamic Logic parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.
Differential Dynamic Logic parser reads input strings in the concrete syntax of differential dynamic logic of KeYmaera X.
Parsing formulas from strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply:
val parser = DLParser val fml0 = parser("x!=5") val fml1 = parser("x>0 -> [x:=x+1;]x>1") val fml2 = parser("x>=0 -> [{x'=2}]x>=0") // parse only formulas val fml3 = parser.formulaParser("x>=0 -> [{x'=2}]x>=0") // parse only programs/games val prog1 = parser.programParser("x:=x+1;{x'=2}") // parse only terms val term1 = parser.termParser("x^2+2*x+1")
- See also
Example: - object DLParserUtils
- object Declaration extends Serializable
-
object
EOF extends Terminal
End Of Stream
- object ExpressionMode extends LexerMode
-
object
FullPrettyPrinter extends BasePrettyPrinter
Fully-parenthesized pretty printer in full form with full parentheses.
Fully-parenthesized pretty printer in full form with full parentheses.
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)
- See also
Example: -
object
FullPrettyPrinter0 extends KeYmaeraXPrinter
Fully parenthesized pretty printer that is functionally equivalent to FullPrettyPrinter
-
object
InterpretedSymbols
List of built-in interpreted function symbols.
-
object
KeYmaera3PrettyPrinter extends KeYmaeraXPrecedencePrinter
Differential Dynamic Logic pretty printer in concrete KeYmaera 3 notation.
-
object
KeYmaeraXArchiveParser extends KeYmaeraXArchiveParserBase
Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers.
Splits a KeYmaera X archive into its parts and forwards to respective problem/tactic parsers. An archive contains at least one entry combining a model in the
.kyxformat and possibly a (partial) proof tactic.Format example:
ArchiveEntry "Entry 1". Description "optional description text". ProgramVariables ... End. Definitions ... End. Problem ... End. Tactic "Proof 1" ... End. Tactic "Proof 2" ... End. End. ArchiveEntry "Entry 2". ... End.
- See also
- object KeYmaeraXArchivePrinter
-
object
KeYmaeraXAxiomParser extends (String) ⇒ List[(String, Formula)] with Logging
Parse an axiom string to a list of named formulas that are to be used as axioms in a theory.
Parse an axiom string to a list of named formulas that are to be used as axioms in a theory. Created by nfulton on 6/11/15.
- See also
-
object
KeYmaeraXExtendedLemmaParser extends (String) ⇒ (Option[String], Provable, List[Evidence]) with Logging
Parses lemma string representations from the following lemma format:
Parses lemma string representations from the following lemma format:
Lemma "<
>" . "<Created by smitsch on 7/03/15. Modified by nfulton on 12/16/15 -- Lemmas are now more general.
-
object
KeYmaeraXLexer extends (String) ⇒ List[Token] with Logging
Lexer for KeYmaera X turns string into list of tokens.
-
object
KeYmaeraXNoContractPrettyPrinter extends KeYmaeraXPrecedencePrinter
KeYmaera X Pretty Printer without contract checking
KeYmaera X Pretty Printer without contract checking
-
object
KeYmaeraXOmitInterpretationPrettyPrinter extends KeYmaeraXOmitInterpretationPrettyPrinter
A pretty printer that omits the interpretations of interpreted functions.
- object KeYmaeraXParser extends KeYmaeraXParser
-
object
KeYmaeraXPrettyPrinter extends KeYmaeraXPrecedencePrinter
Default KeYmaera X Pretty Printer formats differential dynamic logic expressions
Default KeYmaera X Pretty Printer formats differential dynamic logic expressions
-
object
KeYmaeraXStoredProvableParser extends (String) ⇒ List[Sequent]
Parses provable strings in the format stored by edu.cmu.cs.ls.keymaerax.core.Provable.toStorageString().
-
object
LeftAssociative extends BinaryNotation
Left-associative infix operators of arity 2, i.e.
Left-associative infix operators of arity 2, i.e.
x-y-z=(x-y)-z - object LemmaFileMode extends LexerMode
- object LexException
-
object
MixedBinary extends BinaryNotation
Mixed binary operators of arity 2
-
object
NonAssociative extends BinaryNotation
Non-associative infix operators of arity 2, i.e.
Non-associative infix operators of arity 2, i.e. explicit parentheses
a<->(b<->c) - object ODEToInterpreted
-
object
OpSpec
Differential Dynamic Logic's concrete syntax: operator notation specifications.
Differential Dynamic Logic's concrete syntax: operator notation specifications.
- Note
Subtleties: sPower right associative to ensure
x23==x(23)instead of(x2)3. sPower < sNeg to ensure-x2instead of==-(x2)(-x)^2. NUMBER lexer does not contain - sign to enablex-5to be parsed. Parser will make up for this, respecting binary versus unary operators. sEquiv nonassociative to ensure thatp()<->q()<->r()does not parse since binding unclear. sAnd and sOr are right-associative to simplify stable position ordering during sequent decomposition.
- object ParseException extends Serializable
- object Parser extends (String) ⇒ Expression
- object ParserHelper
-
object
ParserInit
Initializes the parser.
-
object
PostfixFormat extends UnaryNotation
Unary postfix operators of arity 1 within syntactic category
-
object
PrefixFormat extends UnaryNotation
Unary prefix operators of arity 1 within syntactic category
- object ProblemFileMode extends LexerMode
- object Region extends Serializable
-
object
ReservedSymbols
List of reserved symbols.
-
object
RightAssociative extends BinaryNotation
Right-associative infix operators of arity 2, i.e.
Right-associative infix operators of arity 2, i.e.
xyz=x(yz) -
object
SequentParser
Parses sequents of the form
ante_1, ante_2, ..., ante_n ==> succ_1, ..., succ_n - object StoredProvableMode extends LexerMode
-
object
StringConverter
Implicit conversions from strings into core data structures.
Implicit conversions from strings into core data structures. Created by smitsch on 1/8/15.
-
object
SubstitutionParser
Parses substitutions.
-
object
TacticReservedSymbols
Lists function symbols that have special meaning in tactics.
- object TernaryOpSpec extends Serializable
-
object
TernaryPrefixFormat extends TernaryNotation
Ternary operators with a terminal before each operand, like if P then a else b
- object UnaryOpSpec extends Serializable
- object UnificationSubstitutionParser
- object UnitOpSpec extends Serializable
- object UnknownLocation extends Location
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 structuresExpression- Differential dynamic logic expressions:Term,Formula,ProgramSequent- Sequents of formulasProvable- Proof certificates transformed by rules/axiomsRule- Proof rules as well asUSubstOnefor (one-pass) uniform substitutions and renaming.StaticSemantics- Static semantics with free and bound variable analysisKeYmaeraXParser.edu.cmu.cs.ls.keymaerax.parser- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser- Parser reading KeYmaera X model and proof archive.kyxfilesDLParser- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser- Combinator parser reading KeYmaera X model and proof archive.kyxfilesedu.cmu.cs.ls.keymaerax.infrastruct- Prover infrastructure outside the kernelUnificationMatch- Unification algorithmRenUSubst- 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 functionalityExpressionTraversal- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon- Bellerophon tactic language and tactic interpreterBelleExpr- Tactic language expressionsSequentialInterpreter- Sequential tactic interpreter for Bellerophon tacticsedu.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 logicSequentCalculus- Sequent Calculus for propositional and first-order logicHybridProgramCalculus- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus- 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 conclusionsedu.cmu.cs.ls.keymaerax.lemma- Lemma mechanismLemma- 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 solversMathematicaQETool- 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-helpto obtain usage informationedu.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