Email Gateway (Aug 19 2022 at 08:26): Email Gateway (Aug 19 2022 at 08:26):From: Jan Keller <Jan@Familie-Keller.org>
Hello,
I am a student in the 6th semster on TU Darmstadt and writing on my
bachelor thesis about proof management for KeY
<http://www.key-project.org/>. My mentor implemented the tool Visual
DbC. It visualize Java code with JML contracts in a diagram based on the
UML standard.
I added associations for all dependencies of prooves, identify changes
in the Java code and JML contracts and compute wether a proof is
deprecated or still valid.
I have a few Qestions for my related work section:
How do you do the management of proofs in Isabelle? Are there any tools?
Are there technics to react on changes of potential dependencies of
proof? Could you detect wether a proof is still valid or deprecated?
Are there tools for the dependencies of proofs? How are the dependencies
visualized? I saw something like a dependency graph in JEdit. Is that
correct?
Have you tools to refractor proofs or requirements?
Thank you for taking the time to answer my questions. I look forward to
your response.
Jan Keller
smime.p7s
Email Gateway (Aug 19 2022 at 08:46):From: Makarius <makarius@sketis.net>
On Wed, 29 Aug 2012, Jan Keller wrote:
How do you do the management of proofs in Isabelle? Are there any tools?
Are there technics to react on changes of potential dependencies of
proof? Could you detect wether a proof is still valid or deprecated?
This is mainly part of the implicit "document model" of the prover, which
is then connected to jEdit via conventional text editing operations
(insert/remove intervals of text). The document model is declarative in
the sense that it reacts on changes in a (hopefully) sensible way. The
hard work of managing dependencies is in the core implementation, both
src/Pure/PIDE/document.ML and document.scala.
The main result of document processing is a markup tree that is associated
with the original source text. By querying that information (via a
document "snapshot") one can get some dependency-like information, say
where formal entities are defined and references. This is how hyperlinks
work in Isabelle/jEdit.
Are there tools for the dependencies of proofs? How are the dependencies
visualized? I saw something like a dependency graph in JEdit. Is that
correct? Have you tools to refractor proofs or requirements?
Most of that is still missing. I am already glad to have most of the
ascyncronous editing model running after several years of working on the
concepts and implementation.
What is coming in the next release is some offline dependency management
as part of Isabelle/Scala, to figure out which source files contribute to
an Isabelle "session" (say HOL or an application of it), and to figure out
changes here wrt. a persistent state in the file-system.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC