package codegen
Code-generation tools to generate C-Code etc. from expressions.
- To do
Stub. Describe for real.
- Alphabetic
- By Inheritance
- codegen
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- case class CAbs(c: CTerm) extends CTerm with Product with Serializable
- case class CAnd(l: CFormula, r: CFormula) extends CFormula with Product with Serializable
- case class CAndProgram(l: CProgram, r: CProgram) extends CProgram with Product with Serializable
- trait CComment extends AnyRef
-
class
CControllerGenerator extends CodeGenerator
Generates a controller from a hybrid program without loops and ODEs.
Generates a controller from a hybrid program without loops and ODEs. A controller transforms an input state by choosing control set values depending on inputs and parameters.
-
class
CControllerSandboxGenerator extends CodeGenerator
Generates a controller sandbox from a hybrid program without loops and ODEs.
Generates a controller sandbox from a hybrid program without loops and ODEs. A controller sandbox safeguards control decisions with a controller monitor by switching to a fallback controller upon controller monitor violation.
-
class
CDetControllerGenerator extends CodeGenerator
Generates a controller from a hybrid program with only deterministic statements.
Generates a controller from a hybrid program with only deterministic statements. A controller transforms an input state by choosing control set values depending on inputs and parameters.
- case class CDivide(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CEqual(l: CTerm, r: CTerm) extends CFormula with Product with Serializable
- case class CError(id: Int, retVal: CExpression, msg: String) extends CProgram with Product with Serializable
-
trait
CExpression extends AnyRef
C expressions.
-
class
CExpressionIntervalLaTeXLogPrettyPrinter extends (CExpression) ⇒ String
Prints C expressions that keep track of the reason for their value.
Prints C expressions that keep track of the reason for their value. NOT interval arithmetic, intervals are for comparisons and formulas. Logs original formula and does unverified metric conversion to measure safety.
-
class
CExpressionLogPrettyPrinter extends (CExpression) ⇒ (String, String)
Prints C expressions that keep track of the reason for their value.
-
class
CExpressionPlainPrettyPrinter extends (CExpression) ⇒ (String, String)
Prints expressions in plain C.
- trait CFormula extends CExpression
- case class CFormulaComment(comment: String) extends CFormula with CComment with Product with Serializable
-
class
CFormulaTermGenerator extends FormulaTermGenerator
Generates formula and term evaluation C code.
Generates formula and term evaluation C code.
termContainer
configures the location where primitive terms are looked up (e.g., structs). -
class
CGenerator extends CodeGenerator
C++ code generator that prints a file header, include statements, declarations, and the output of
bodyGenerator
. - case class CGreater(l: CTerm, r: CTerm) extends CFormula with Product with Serializable
- case class CGreaterEqual(l: CTerm, r: CTerm) extends CFormula with Product with Serializable
- case class CIfThenElse(f: CFormula, ifP: CProgram, elseP: CProgram) extends CProgram with Product with Serializable
- case class CLess(l: CTerm, r: CTerm) extends CFormula with Product with Serializable
- case class CLessEqual(l: CTerm, r: CTerm) extends CFormula with Product with Serializable
- case class CMax(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CMin(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CMinus(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
-
class
CMonitorGenerator extends MonitorGenerator
Generates a monitor from a ModelPlex expression.
- class CMpfrControllerGenerator extends CodeGenerator
-
class
CMpfrPrettyPrinter extends (CExpression) ⇒ (String, String)
Pretty prints expressions with the GNU MPFR library operators.
- case class CNeg(c: CTerm) extends CTerm with Product with Serializable
- case class CNot(c: CFormula) extends CFormula with Product with Serializable
- case class CNotEqual(l: CTerm, r: CTerm) extends CFormula with Product with Serializable
- case class CNumber(n: BigDecimal) extends CTerm with Product with Serializable
- case class COr(l: CFormula, r: CFormula) extends CFormula with Product with Serializable
- case class COrProgram(l: CProgram, r: CProgram) extends CProgram with Product with Serializable
- case class CPair(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CPlus(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CPower(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CPredicate(name: String, arg: CTerm) extends CFormula with Product with Serializable
- trait CProgram extends CExpression
- case class CProgramComment(comment: String) extends CProgram with CComment with Product with Serializable
- case class CReturn(e: CExpression) extends CProgram with Product with Serializable
- trait CTerm extends CExpression
- case class CTermComment(comment: String) extends CTerm with CComment with Product with Serializable
- case class CTimes(l: CTerm, r: CTerm) extends CTerm with Product with Serializable
- case class CUnaryFunction(name: String, arg: CTerm) extends CTerm with Product with Serializable
- case class CVariable(name: String) extends CTerm with Product with Serializable
- class CodeGenerationException extends Exception
-
trait
CodeGenerator extends (Expression) ⇒ (String, String)
Generate executable code from a differential dynamic logic expression.
Generate executable code from a differential dynamic logic expression. Returns a tuple (Definitions, Body), where
body
computesexpression
using the sub-routines indefinitions
. -
trait
CodePrettyPrinter extends (CExpression) ⇒ (String, String)
Pretty-prints expressions to code.
Pretty-prints expressions to code. Returns a tuple of (declarations used in code, code).
-
abstract
class
FormulaTermGenerator extends CodeGenerator
Generates formula and term evaluation code.
Generates formula and term evaluation code.
termContainer
configures the location where primitive terms are looked up (e.g., structs, classes). -
class
GenericFormulaTermGenerator extends FormulaTermGenerator
Converts formulas and terms according to
prettyPrinter
.Converts formulas and terms according to
prettyPrinter
. UsestermContainer
to refer to arguments. -
abstract
class
MonitorGenerator extends CodeGenerator
Base class for monitor generators.
Base class for monitor generators. Prints expressions with
prettyPrinter
, accesses expressions according to termContainer (e.g.,params.x
orparams->x
). - class PythonExpressionPrettyPrinter extends (CExpression) ⇒ (String, String)
-
class
PythonGenerator extends CodeGenerator
Python code generator that prints a file header, include statements, declarations, and the output of
bodyGenerator
. -
class
PythonMonitorGenerator extends MonitorGenerator
Generates a monitor from a ModelPlex expression.
-
class
SimpleMonitorGenerator extends MonitorGenerator
Generates a monitor expression without surrounding function head, comments.
-
class
PythonFormulaTermGenerator extends FormulaTermGenerator
Generates formula and term evaluation C code.
Generates formula and term evaluation C code.
termContainer
configures the location where primitive terms are looked up (e.g., structs).- Annotations
- @deprecated
- Deprecated
Use GenericFormulaTermGenerator instead
Value Members
- object CFalse extends CFormula
-
object
CFormulaTermGenerator
Conversion of names.
- object CGenerator
- object CMonitorGenerator
- object CNoop extends CProgram
- object CNothing extends CTerm with Product with Serializable
-
object
CPrettyPrinter extends CodePrettyPrinter
Prints C expressions.
- object CTrue extends CFormula
- object CodeGenerator
-
object
PythonGenerator
Python code generator header and declaration printing.
- object PythonMonitorGenerator
- object PythonPrettyPrinter extends CodePrettyPrinter
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
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (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.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.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-help
to 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