object DebuggingTactics
- Alphabetic
- By Inheritance
- DebuggingTactics
- AnyRef
- Any
- Hide All
- Show All
- 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
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
assert(cond: (Sequent, Position) ⇒ Boolean, message: ⇒ String): BuiltInPositionTactic
assert is a no-op tactic that raises a tactic assertion error if the provable does not satisfy a condition at position pos.
-
def
assert(cond: (Sequent, Position) ⇒ Boolean, message: ⇒ String, ex: (String) ⇒ Throwable): BuiltInPositionTactic
assert is a no-op tactic that raises an error if the provable does not satisfy a condition at position pos.
-
def
assert(cond: (Sequent) ⇒ Boolean, message: ⇒ String): BuiltInTactic
assert is a no-op tactic that raises a tactic assertion error if the provable does not satisfy a condition on the sole subgoal.
-
def
assert(cond: (Sequent) ⇒ Boolean, message: ⇒ String, ex: (String) ⇒ Throwable): BuiltInTactic
assert is a no-op tactic that raises an error if the provable does not satisfy a condition on the sole subgoal.
-
def
assert(fml: Formula, message: ⇒ String): DependentPositionWithAppliedInputTactic
assert is a no-op tactic that raises a tactic assertion error if the provable has not the expected formula at the specified position.
-
def
assert(fml: Formula, message: ⇒ String, ex: (String) ⇒ Throwable): DependentPositionWithAppliedInputTactic
assert is a no-op tactic that raises an error if the provable has not the expected formula at the specified position.
-
def
assert(anteSize: Int, succSize: Int, msg: ⇒ String = ""): BuiltInTactic
assert is a no-op tactic that raises a tactic assertion error if the provable is not of the expected size.
-
def
assert(anteSize: Int, succSize: Int, msg: ⇒ String, ex: (String) ⇒ Throwable): BuiltInTactic
assert is a no-op tactic that raises an error if the provable is not of the expected size.
- def assertAt(msg: ⇒ String, assertion: (Expression) ⇒ Boolean, ex: (String) ⇒ Throwable): BuiltInPositionTactic
-
def
assertAt(msg: (Expression) ⇒ String, assertion: (Expression) ⇒ Boolean, ex: (String) ⇒ Throwable = new TacticAssertionError(_)): BuiltInPositionTactic
Assert that the assertion holds at a the specified position.
Assert that the assertion holds at a the specified position. Could be a non-top-level position. Analogous to debugAt.
- msg
The message to display.
- assertion
The assertion.
-
def
assertE(expected: ⇒ Expression, message: ⇒ String): DependentPositionWithAppliedInputTactic
assertE is a no-op tactic that raises a tactic assertion error if the provable has not the expected expression at the specified position.
-
def
assertE(expected: ⇒ Expression, message: ⇒ String, ex: (String) ⇒ Throwable): DependentPositionWithAppliedInputTactic
assertE is a no-op tactic that raises an error if the provable has not the expected expression at the specified position.
-
def
assertOnAll(cond: (Sequent) ⇒ Boolean, message: ⇒ String, ex: (String) ⇒ Throwable = new TacticAssertionError(_)): BuiltInTactic
assertOnAll is a no-op tactic that raises an error the provable does not satisfy a condition on all subgoals.
-
def
assertProvableSize(provableSize: Int, ex: (String) ⇒ Throwable = new TacticAssertionError(_)): BuiltInTactic
asserts that the provable has
provableSize
many subgoals. -
def
assertX(expected: Expression, msg: String): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( ("Assert", "assert") , "assert" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
debug(message: ⇒ String, doPrint: Boolean = DEBUG, printer: (ProvableSig) ⇒ String = _.toString): BuiltInTactic
debug is a no-op tactic that prints a message and the current provable, if doPrint (defaults to the system property DEBUG) is true.
-
def
debugAt(message: ⇒ String, doPrint: Boolean = DEBUG): BuiltInPositionTactic
debug is a no-op tactic that prints a message and the current provable, if the system property DEBUG is true.
-
def
debugX(msg: String): StringInputTactic
- Annotations
- @Tactic( ("Debug", "debug") , "debug" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
-
def
done(msg: Option[String], lemmaName: Option[String]): StringInputTactic
- Annotations
- @Tactic( ("Done","done") , "done" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- def done(msg: String, storeLemma: Option[String]): StringInputTactic
- def done(msg: String): StringInputTactic
-
lazy val
done: BelleExpr
- See also
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
error(s: ⇒ String, e: (String) ⇒ BelleThrowable = new TacticInapplicableFailure(_)): BuiltInTactic
Indicates a failed attempt that triggers proof search.
- def error(e: Throwable): BuiltInTactic
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
pending(tactic: String): StringInputTactic
Placeholder for a tactic string that is not executed.
Placeholder for a tactic string that is not executed.
- Annotations
- @Tactic( "pending" , "pending" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
-
def
pendingX(tactic: String): StringInputTactic
- Annotations
- @Tactic( "pendingX" , "pendingX" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
-
def
print(message: ⇒ String): BuiltInTactic
print is a no-op tactic that prints a message and the current provable, regardless of DEBUG being true or false
-
def
printIndexed(message: ⇒ String): BuiltInTactic
printIndexed is a no-op tactic that prints a message and the current provable (verbose sequent with formula indices), regardless of DEBUG being true or false
-
def
printX(msg: String): StringInputTactic
- Annotations
- @Tactic( ("Print", "print") , "print" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
- def recordQECall(): BuiltInTactic
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
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( ... )
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