index.md 8.9 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1 2
<style>
        #content {
Alexander Weigl's avatar
Alexander Weigl committed
3
            width: 50em;
Alexander Weigl's avatar
Alexander Weigl committed
4 5 6 7 8 9 10 11 12 13
            margin: auto;
            border: 1px #ccc solid;
            border-bottom-left-radius: 2em;
            border-top-right-radius: 2em;
            background: ghostwhite;
            padding: 2em;
        }

        .column>div{
            float: left;
Alexander Weigl's avatar
Alexander Weigl committed
14 15
            width: 30%;
            margin:1%;
16
            text-align: left;
Alexander Weigl's avatar
Alexander Weigl committed
17 18 19 20 21 22
        }

        .column img {
            width: 150px;
            text-align: center;
        }
Alexander Weigl's avatar
Alexander Weigl committed
23 24
        
        img.thumb {
Alexander Weigl's avatar
Alexander Weigl committed
25
            width:100%;           
Alexander Weigl's avatar
Alexander Weigl committed
26
            border-radius:50%;
Alexander Weigl's avatar
Alexander Weigl committed
27
        }
Alexander Weigl's avatar
Alexander Weigl committed
28 29
       
       .column h3 {
Alexander Weigl's avatar
Alexander Weigl committed
30
            text-align:center;
Alexander Weigl's avatar
Alexander Weigl committed
31 32 33
       }
       
       div.feature-caption {
Alexander Weigl's avatar
Alexander Weigl committed
34
           text-align: block;           
Alexander Weigl's avatar
Alexander Weigl committed
35 36
           text-align: justify;
           font-size: 80%;
Alexander Weigl's avatar
Alexander Weigl committed
37
           font-weight:bold;
Alexander Weigl's avatar
Alexander Weigl committed
38 39
       }
       
Alexander Weigl's avatar
Alexander Weigl committed
40 41
</style>

Alexander Weigl's avatar
Alexander Weigl committed
42
# Proof Script Debugger for the KeY System
Alexander Weigl's avatar
Alexander Weigl committed
43

Alexander Weigl's avatar
Alexander Weigl committed
44
The proof script debugger is a prototypical implementation
Alexander Weigl's avatar
Alexander Weigl committed
45 46 47
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
48
[KeY](http://www.key-project.org). KeY is an interactive program verification
Alexander Weigl's avatar
Alexander Weigl committed
49 50
system for Java program annotated with the Java Modeling Language (JML).

Alexander Weigl's avatar
Alexander Weigl committed
51

Alexander Weigl's avatar
Alexander Weigl committed
52 53
The protypical implementation includes a proof scripting language that is tailored to the
problem domain of program verification.
54
The main features of the language are:
Alexander Weigl's avatar
Alexander Weigl committed
55 56

1. integration of domain specific entities like goal, formula, term and rule as
57
first-class citizens into the language;</li>
Alexander Weigl's avatar
Alexander Weigl committed
58
1. an expressive proof goal selection mechanism
Sarah Grebing's avatar
Sarah Grebing committed
59 60 61
    - 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
Alexander Weigl's avatar
Alexander Weigl committed
62 63 64 65
1. a repetition construct which allows repeated application of proof strategies;</li>
1. support for proof exploration within the language.</li>


Alexander Weigl's avatar
Alexander Weigl committed
66 67 68
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.
69

Alexander Weigl's avatar
Alexander Weigl committed
70 71 72
## Publications

A full description of the language and debugging-concept 
Sarah Grebing's avatar
Sarah Grebing committed
73 74 75
is published at [HVC 2017](http://rdcu.be/E4fF). 
A short tool description is also [available](
http://arxiv.org/abs/1804.04402).
Alexander Weigl's avatar
Alexander Weigl committed
76

Sarah Grebing's avatar
Sarah Grebing committed
77 78
## Debugging Script for Quicksort's `split` method.

79 80 81 82 83 84 85 86 87 88 89 90 91 92
### Selecting the proof script
<center>
<video width="80%"  controls>
  <source src="../psdbg_videos/selection.webm" type="video/webm">
Your browser does not support the video tag.
</video>
</center>

In this video the selection of the Quicksort example from the paper is shown.
After loading the example a dialog appears in which the appropriate contract for the 
Java method `split` has to be selected. After loading the problem the program to be verified is 
shown in an own view on the right side, the script is shown on the left side and in the middle the proof obligation and the list of open goals is shown. 
Views can be selected and docked to other places on the screen.

Sarah Grebing's avatar
Sarah Grebing committed
93
Please note that after a succesful load the statusbar indicates that the contract was loaded.
94 95

### Setting a breakpoint and starting the Interpreter
Alexander Weigl's avatar
Alexander Weigl committed
96 97

<center>
98 99 100 101 102 103 104 105 106 107
<video width="80%"  controls>
  <source src="../psdbg_videos/breakpoint.webm" type="video/webm">
Your browser does not support the video tag or WebM.
</video>
</center>

In this video it is shown how to set a breakpoint and how to start the debugger/interpreter. Please note that if no script is set as main script the first script in the open editor is taken as main script an set. This can be seen in the status bar.
Furthermore the status of the interprter is shown with small icons in the right lower corner of the status bar. A running interpreter is indicated by a running figure. A paused interpreter is indicated by a timer. 
If the interpreter reaches the end of the proof script the status is shown as a tick.
The video does not include the full execution until the breakpoint, as executing certain proof commands may take time.
Sarah Grebing's avatar
Sarah Grebing committed
108

109 110
### Stepping into, over and reverse and continue
<center>
Alexander Weigl's avatar
Alexander Weigl committed
111
<video width="80%"  controls>
112
  <source src="../psdbg_videos/stepping_new.webm" type="video/webm">
Alexander Weigl's avatar
Alexander Weigl committed
113 114 115
Your browser does not support the video tag or WebM.
</video>
</center>
116

117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
After reaching the breakpoint set in the video before, we are left with 4 open goals, visible in the goal list.
In this video the stepping functionalities are demonstrated. Stepping into proof commands of the underlying verification system
results in a view of the partial proof tree corresponding to the execution of this command.
It can also be seen to which sequents the matching expression matches. 

### Successful Proof Indication
<center>
<video width="80%"  controls>
  <source src="../psdbg_videos/proof_new.webm" type="video/webm">
Your browser does not support the video tag or WebM.
</video>
</center>

In this video the successful proof is shown and it is demonstrated how to access the full proof tree of the proof for the `split` method.

### SequentMatcher and Interactive Rule Application
<center>
<video width="80%"  controls>
  <source src="../psdbg_videos/interactive.webm" type="video/webm">
Your browser does not support the video tag or WebM.
</video>
</center>

Sarah Grebing's avatar
Sarah Grebing committed
140
In this video we demonstrate the interactive point and click rule applications after selecting the interactive button. We further demonstrate how the interaction is included to the original script.
141 142 143 144 145 146 147 148 149 150 151 152 153

<center>
<video width="80%"  controls>
  <source src="../psdbg_videos/sequentmatcher.webm" type="video/webm">
Your browser does not support the video tag or WebM.
</video>
</center>

Furthermore, we show how to use our SequentMatcher Window to enhance the auto-generated matching expressions from the 
interactive rule applications.



Alexander Weigl's avatar
Alexander Weigl committed
154
## Features
Alexander Weigl's avatar
Alexander Weigl committed
155 156

<div class="column">
Alexander Weigl's avatar
Alexander Weigl committed
157
    <div>
158
        <h3>Inspection of different parts of the proof state</h3>
159
        <p> 
160 161
        The different parts of the proof state can be inspected:
        <ul>
Alexander Weigl's avatar
Alexander Weigl committed
162 163 164 165
        <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>
166
        </p> 
Alexander Weigl's avatar
Alexander Weigl committed
167 168
    </div>
    <div >
169
        <h3>Adjustable view on list of open goals</h3>
Alexander Weigl's avatar
Alexander Weigl committed
170
        <img class="thumb" src="img/thumb_ScreenshotGoalList.png" />
Alexander Weigl's avatar
Alexander Weigl committed
171
        <div class="feature-caption"/></div>
Alexander Weigl's avatar
Alexander Weigl committed
172 173
    </div>
    <div >
174
        <h3>Explore the proof tree of KeY</h3>
Alexander Weigl's avatar
Alexander Weigl committed
175 176
        <img class="thumb" src="img/thumb_ScreenshotProofTree.png"/>
        <div class="feature-caption"/></div>
Alexander Weigl's avatar
Alexander Weigl committed
177 178 179
    </div>
</div>
<div style="clear: both;"/>
Alexander Weigl's avatar
Alexander Weigl committed
180 181 182 183 184 185 186

<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.
Alexander Weigl's avatar
Alexander Weigl committed
187
        </div>
Alexander Weigl's avatar
Alexander Weigl committed
188 189 190 191 192 193 194
    </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
195
            and then Back to the Future, again!
Alexander Weigl's avatar
Alexander Weigl committed
196 197
        </div>
    </div>
Alexander Weigl's avatar
Alexander Weigl committed
198 199 200 201 202 203 204
    <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>
Alexander Weigl's avatar
Alexander Weigl committed
205 206 207 208
</div>

<div style="clear: both;"/> 

Alexander Weigl's avatar
Alexander Weigl committed
209
<h2>Downloads</h2>
Alexander Weigl's avatar
Alexander Weigl committed
210

Alexander Weigl's avatar
Alexander Weigl committed
211
<ul>
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
 <li>PSDBG - <strong>Experimental Version</strong>
    <a href="../psdbg_releases/psdbg-Experimental-1.1.jar">psdbg-Experimental-1.1.jar</a>
    <br>
    This version is an experimental development version of PSDBG, including examples. 
    Its enhancements are based on an evaluation of the first version.
    Not all provided features in this version may be completely functional yet. 
    <br>
    One major change is the syntax for Matching Expressions. The wildcard symbol is now "?" instead of "_".
    <br>
     Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
    <br>
    <a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
    <a href="thirdparty.txt">Third Party Licenses</a> 
    <br>
    Executable with <code>java -jar psdbg-Experimental-1.1.jar</code>
    </li>
Sarah Grebing's avatar
Sarah Grebing committed
228 229
 <li>PSDBG - <strong>Version 1.0.2c-FM</strong> 
    <a href="../psdbg_releases/psdbg-1.0.2c-fm.jar">psdbg-1.0.2c-fm.jar</a>
Alexander Weigl's avatar
Alexander Weigl committed
230
    <br>
Sarah Grebing's avatar
Sarah Grebing committed
231
    First implementation of PSDBG, including examples.
232
    <br>
233
     Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
234
    <br>
235
    <a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
Alexander Weigl's avatar
Alexander Weigl committed
236 237
    <a href="thirdparty.txt">Third Party Licenses</a> 
    <br>
Sarah Grebing's avatar
Sarah Grebing committed
238
    Executable with <code>java -jar psdbg-1.0.2c-fm.jar</code>
Alexander Weigl's avatar
Alexander Weigl committed
239 240
 </li>
</ul>
Alexander Weigl's avatar
Alexander Weigl committed
241 242

<div style="clear: both;"/>
Sarah Grebing's avatar
Sarah Grebing committed
243