class InMemoryDB extends DBAbstraction
In-memory database, e.g., for stepping into tactics.
- Alphabetic
- By Inheritance
- InMemoryDB
- DBAbstraction
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new InMemoryDB()
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
addAgendaItem(proofId: Int, initialProofNode: ProofTreeNodeId, displayName: String): Int
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
addAlternative(alternativeTo: Int, inputProvable: ProvableSig, trace: ExecutionTrace): Unit
Truncate the execution trace at the beginning of alternativeTo and replace it with trace.
Truncate the execution trace at the beginning of alternativeTo and replace it with trace.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
addBelleExpr(expr: BelleExpr): Int
Adds a Bellerophon expression as an executable and returns the new executableId
Adds a Bellerophon expression as an executable and returns the new executableId
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
addExecutionStep(step: ExecutionStepPOJO): Int
Adds an execution step to an existing execution
Adds an execution step to an existing execution
- Definition Classes
- InMemoryDB → DBAbstraction
- Note
Implementations should enforce additional invarants -- never insert when branches or alt orderings overlap.
-
def
addModelTactic(modelId: String, fileContents: String): Option[Int]
Adds a tactic script to the model
Adds a tactic script to the model
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
agendaItemsForProof(proofId: Int): List[AgendaItemPOJO]
- Definition Classes
- InMemoryDB → DBAbstraction
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
checkPassword(username: String, password: String): Boolean
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
cleanup(): Unit
Initializes a new database.
Initializes a new database.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
createModel(userId: String, name: String, fileContents: String, date: String, description: Option[String] = None, publink: Option[String] = None, title: Option[String] = None, tactic: Option[String] = None): Option[Int]
Creates a new model in the database if
namedoes not exist yet.Creates a new model in the database if
namedoes not exist yet. Returns the ID of the created model. Otherwise (if the model name is used already) returns None and the database is unmodified.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
createProof(provable: ProvableSig): Int
Create a temporary proof without model, starting from 'provable'.
Create a temporary proof without model, starting from 'provable'.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
createProofForModel(modelId: Int, name: String, description: String, date: String, tactic: Option[String]): Int
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
createProofForModel(modelId: String, name: String, description: String, date: String, tactic: Option[String]): String
- Definition Classes
- DBAbstraction
-
def
createProvable(p: ProvableSig): Int
Stores a Provable in the database and returns its ID
Stores a Provable in the database and returns its ID
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
createUser(username: String, password: String, mode: String): Unit
Creates a new user, identified by the unique
usernamewithpassword.Creates a new user, identified by the unique
usernamewithpassword. The user belongs to groupgroup.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
deleteExecutionStep(proofId: Int, stepId: Int): Unit
Deletes execution steps.
Deletes execution steps.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
deleteModel(modelId: Int): Boolean
Deletes this model and all associated proofs.
Deletes this model and all associated proofs.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
deleteProof(proofId: Int): Boolean
Deletes the proof.
Deletes the proof.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
deleteProofSteps(executionId: Int): Int
Deletes the recorded proof steps, but keeps the proof and its tactic.
Deletes the recorded proof steps, but keeps the proof and its tactic. Returns the number of deleted steps.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
deleteProvable(provableId: Int): Boolean
Deletes a provable and all associated sequents / formulas
Deletes a provable and all associated sequents / formulas
- Definition Classes
- InMemoryDB → DBAbstraction
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
getAgendaItem(proofId: Int, initialProofNode: ProofTreeNodeId): Option[AgendaItemPOJO]
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getAllConfigurations: Set[ConfigurationPOJO]
- Definition Classes
- InMemoryDB → DBAbstraction
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getConfiguration(configName: String): ConfigurationPOJO
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getExecutable(executableId: Int): ExecutablePOJO
Returns the executable with ID executableId
Returns the executable with ID executableId
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getExecutables(executableIds: List[Int]): List[ExecutablePOJO]
Allow retrieving executables in bulk to reduce the number of database queries.
-
def
getExecutionStep(proofId: Int, stepId: Int): Option[ExecutionStep]
Returns the execution step with id
stepIdof proofproofIdwith all provables etc.Returns the execution step with id
stepIdof proofproofIdwith all provables etc. filled in.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getExecutionSteps(executionId: Int): List[ExecutionStepPOJO]
Return a list of all finished execution steps in the current history of the execution, in the order in which they occurred.
Return a list of all finished execution steps in the current history of the execution, in the order in which they occurred.
- Definition Classes
- InMemoryDB → DBAbstraction
- Note
For most purposes, getExecutionTrace is more convenient, but slower.
-
def
getExecutionTrace(proofId: Int, withProvables: Boolean = true): ExecutionTrace
Return the sequence of steps that led to the current state of the proof.
Return the sequence of steps that led to the current state of the proof. Loading a trace with provables is slow.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getFirstExecutionStep(proofId: Int): Option[ExecutionStepPOJO]
Returns the first step of the proof
Returns the first step of the proof
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getInvariants(modelId: Int): Map[Expression, Formula]
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getModel(modelId: Int): ModelPOJO
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getModel(modelId: String): ModelPOJO
- Definition Classes
- DBAbstraction
-
def
getModelList(userId: String): List[ModelPOJO]
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getPlainExecutionStep(executionId: Int, stepId: Int): Option[ExecutionStepPOJO]
Returns the execution step with id
stepIdof proofproofIdin plain database form.Returns the execution step with id
stepIdof proofproofIdin plain database form.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getPlainOpenSteps(proofId: Int): List[(ExecutionStepPOJO, List[Int])]
Returns a list of steps that do not have successors for each of their subgoals.
Returns a list of steps that do not have successors for each of their subgoals.
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getPlainStepSuccessors(proofId: Int, prevStepId: Int, branchOrder: Int): List[ExecutionStepPOJO]
Returns the successors of the execution step with id
stepIdof proofproofIdin plain database form.Returns the successors of the execution step with id
stepIdof proofproofIdin plain database form.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getProofInfo(proofId: Int): ProofPOJO
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getProofInfo(proofId: String): ProofPOJO
- Definition Classes
- DBAbstraction
-
def
getProofsForModel(modelId: Int): List[ProofPOJO]
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getProofsForModel(modelId: String): List[ProofPOJO]
- Definition Classes
- DBAbstraction
-
def
getProofsForUser(userId: String): List[(ProofPOJO, String)]
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getProvable(lemmaId: Int): ProvablePOJO
Use escape hatch in prover core to create a new Provable
Use escape hatch in prover core to create a new Provable
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getStepProvable(executionId: Int, stepId: Option[Int], subgoal: Option[Int]): Option[ProvableSig]
Returns the
subgoalof execution stepstepIdof proofproofId; proof conclusion if both None.Returns the
subgoalof execution stepstepIdof proofproofId; proof conclusion if both None.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getTempUsers: List[UserPOJO]
Returns all temporary users (group 3).
Returns all temporary users (group 3).
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getUniqueModelName(userId: String, modelName: String): String
Returns a unique model name by appending an index, if
modelNamealready exists.Returns a unique model name by appending an index, if
modelNamealready exists.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
getUser(username: String): Option[UserPOJO]
Returns the user identified by
username, if any.Returns the user identified by
username, if any.- Definition Classes
- InMemoryDB → DBAbstraction
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
isProofClosed(proofId: Int): Boolean
- Definition Classes
- InMemoryDB → DBAbstraction
- def loadProvables(lemmaIds: List[Int]): List[ProvablePOJO]
-
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
openProofs(userId: String): List[ProofPOJO]
- Definition Classes
- DBAbstraction
- def printStats(): Unit
-
def
proofExists(proofId: Int): Boolean
- Definition Classes
- InMemoryDB → DBAbstraction
- def proofSteps(executionId: Int): List[ExecutionStepPOJO]
-
def
syncDatabase(): Unit
Ensures any changes which might currently reside in auxilliary storage have been synced to main storage.
Ensures any changes which might currently reside in auxilliary storage have been synced to main storage.
- Definition Classes
- InMemoryDB → DBAbstraction
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
def
updateAgendaItem(item: AgendaItemPOJO): Unit
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
updateConfiguration(config: ConfigurationPOJO): Unit
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
updateExecutionStep(executionStepId: Int, step: ExecutionStepPOJO): Unit
Updates an executable step
Updates an executable step
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
updateModel(modelId: Int, name: String, title: Option[String], description: Option[String], content: Option[String], tactic: Option[String]): Unit
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
updateProofInfo(proof: ProofPOJO): Unit
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
updateProofName(proofId: String, name: String): Unit
- Definition Classes
- DBAbstraction
-
def
updateProofName(proofId: Int, name: String): Unit
- Definition Classes
- DBAbstraction
-
def
userExists(username: String): Boolean
- Definition Classes
- InMemoryDB → DBAbstraction
-
def
userOwnsProof(userId: String, proofId: String): Boolean
Indicates whether or not the user
userIdowns the proofproofId.Indicates whether or not the user
userIdowns the proofproofId.- Definition Classes
- InMemoryDB → DBAbstraction
-
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,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