Skip to content

GitLab

P
ProofScriptParser
Commit 3ae847f4 authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Merge remote-tracking branch 'origin/master' 

# Conflicts:
#	rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java
parents 07008761 fb531145
Hide whitespace changes
Inline Side-by-side
Showing with 96 additions and 65 deletions
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java
View file @ 3ae847f4
......@@ -76,7 +76,7 @@ public class ProofTreeManager<T> {
int ctxLength = node.getContext().length;
// We got a step deeper in the ASTNode stack.
// So we a caller
// So we have a caller
if (getContextDepth() < ctxLength) {
pushContext();
intoCurrentContext(node);
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java
View file @ 3ae847f4
......@@ -13,14 +13,14 @@ public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
if (statePointer.getStepInvOver() != null) {
PTreeNode<T> statementBefore = statePointer.getStepInvOver();
dbg.setStatePointer(statementBefore);
} else{
dbg.setStatePointer(statePointer);
} else {
if (statePointer.isLastNode() || statePointer.isFirstNode()) {
System.out.println("We need Sonderbehandlung here");
}
}
}
}
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ 3ae847f4
......@@ -29,6 +29,7 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.application.Platform;
......@@ -506,11 +507,11 @@ public class DebuggerMain implements Initializable {
btnInteractiveMode.setDisable(false);
assert model.getDebuggerFramework() != null;
btnInteractiveMode.setSelected(true);
/*PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
assert statePointer!=null;
State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
*/
});
}
......
website/docs/index.md
View file @ 3ae847f4
<style>
#content {
width: 60em;
margin: auto;
......@@ -12,7 +11,8 @@
.column>div{
float: left;
width: 33%;
width: 30%;
margin:1%;
text-align: left;
}
......@@ -20,95 +20,125 @@
width: 150px;
text-align: center;
}
img.thumb {
width:100%;
border-radius:150px;
}
.column h3 {
}
div.feature-caption {
text-align: block;
text-align: justify;
font-size: 80%;
}
</style>
<h1>Proof Script Debugger for the KeY System</h1>
# Proof Script Debugger for the KeY System
<p>The proof script debugger is a prototypical implementation
The proof script debugger is a prototypical implementation
of an interaction concept for program verification systems that are rule based and
use a program logic.
The prototype is implemented on top of the interactive program verification system
<a href="http://www.key-project.org">KeY</a>. KeY is an interactive program verification
[KeY](http://www.key-project.org. KeY is an interactive program verification
system for Java program annotated with the Java Modeling Language (JML).
</p>
<p>
The protypical implementation includes a proof scripting language that is tailored to the
problem domain of program verification.
The main features of the language are:
<ol>
<li> integration of domain specific entities like goal, formula, term and rule as
1. integration of domain specific entities like goal, formula, term and rule as
first-class citizens into the language;</li>
<li> an expressive proof goal selection mechanism
<ul>
<li>to identify and select individual proof branches,</li>
<li>to easily switch between proof branches,</li>
<li>to select multiple branches for uniform treatment (multi-matching);</li>
</ul>
that is resilient to small changes in the proof</li>
<li> a repetition construct which allows repeated application of proof strategies;</li>
<li> support for proof exploration within the language.</li>
1. an expressive proof goal selection mechanism
* to identify and select individual proof branches,
* to easily switch between proof branches,
* to select multiple branches for uniform treatment (multi-matching);
that is resilient to small changes in the proof
1. a repetition construct which allows repeated application of proof strategies;</li>
1. support for proof exploration within the language.</li>
</ol>
Together with the proof scripting language a debugging concept for failed proof attempts
is implemented that leverages well-known concepts from program debugging to
the analysis of failed proof attempts.
</p>
<h2>Publications</h2>
A full description of the language and debugging-concept is published at <a href="">HVC 2017</a>.
## Publications
<h2>Features</h2>
A full description of the language and debugging-concept
is published at [HVC 2017](hvc2017.pdf)
## Features
<div class="column">
<div >
<div>
<h3>Inspection of different parts of the proof state</h3>
<p>
The different parts of the proof state can be inspected:
<ul>
<li>list of open goals</li>
<li>sequent of selected open goal</li>
<li>path through program (if existing) for selected open goal</li>
</ul>
<li>list of open goals</li>
<li>sequent of selected open goal</li>
<li>path through program (if existing) for selected open goal</li>
</ul>
</p>
</div>
<div >
<h3>Adjustable view on list of open goals</h3>
<img src="img/ScreenshotState.png" style="width:304px;height:228px;" />
<img class="thumb" src="img/thumb_ScreenshotGoalList.png" />
<div class="feature-caption"/></div>
</div>
<div >
<h3>Explore the proof tree of KeY</h3>
<img src="img/ScreenshotProofTree.png" style="width:304px;height:228px;" />
<img class="thumb" src="img/thumb_ScreenshotProofTree.png"/>
<div class="feature-caption"/></div>
</div>
</div>
<div style="clear: both;"/>
<div class="column">
<div >
<h3>Stepwise evaluation of the proof script</h3>
<p>
The proof script can be evaluated stepwise and by running to a set breakpoint.
</p>
</div>
<div >
<h3>Set a breakpoint and run execution to breakpoint</h3>
<img src="img/ScreenshotBreakpoint.png" style="width:304px;height:228px;"/>
<div class="column">
<div>
<h3>Set a breakpoint and run execution to breakpoint</h3>
<img src="img/thumb_ScreenshotBreakpoint.png" class="thumb"/>
<div class="feature-caption">
Mark lines with an (conditional) breakpoint to pause the script execution.
</div>
<div >
<h3> Step forward and step backward</h3>
<img src="img/ScreenshotStep.png" style="width:304px;height:228px;" />
</div>
<div>
<h3>Stepwise evaluation for time travellers</h3>
<img src="img/thumb_ScreenshotStep.png" class="thumb" />
<div class="feature-caption">
Stepwise script execution: step over and into.
Our special offers for time travellers: Go backwards in time
and then Back to the Future,again!
</div>
<div >
<h3> Interactive Rule Application</h3>
<img src="img/ScreenshotInteractive.png" style="width:304px;height:228px;" />
</div>
</div>
<div style="clear: both;"/>
<p>
For Accessing the prototype, please contact the authors.
<footer style="border-top: #ccc 1px solid">
Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
</footer>
</p>
<div>
<h3> Interactive Rule Application</h3>
<img src="img/thumb_ScreenshotInteractive.png" class="thumb" />
<div class="feature-caption">
Select rules for interactive application.
</div>
</div>
</div>
<div style="clear: both;"/>
<h2>Getting Started</h2>
<h2>Downloads</h2>
<ul>
<li>PSDBG - <strong>Version 1.0-FM</strong>
<a href="~/releases/psdbg-1.0-fm.jar">psdbg-1.0-fm.jar</a>
<br>
Special Version for the tool paper at Formal Methods 2018.
</li>
</ul>
<div style="clear: both;"/>
website/mkdocs.yml
View file @ 3ae847f4
......@@ -17,8 +17,8 @@ markdown_extensions:
permalink: True
separator: "_"
- sane_lists
- mdx_math:
enable_dollar_delimiter: True #for use of inline $..$
# - mdx_math:
# enable_dollar_delimiter: True #for use of inline $..$
extra_javascript: ['https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML']
#extra_javascript: ['https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML']
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment