index.md 3.45 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
<style>

        #content {
            width: 60em;
            margin: auto;
            border: 1px #ccc solid;
            border-bottom-left-radius: 2em;
            border-top-right-radius: 2em;
            background: ghostwhite;
            padding: 2em;
        }

        .column>div{
            float: left;
            width: 33%;
Sarah Grebing's avatar
Sarah Grebing committed
16
            text-align: left;
Alexander Weigl's avatar
Alexander Weigl committed
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
        }

        .column img {
            width: 150px;
            text-align: center;
        }
</style>

<h1>Proof Script Debugger for the KeY System</h1>

<p>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
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.
Sarah Grebing's avatar
Sarah Grebing committed
38
The main features of the language are:
Alexander Weigl's avatar
Alexander Weigl committed
39
<ol>
Sarah Grebing's avatar
Sarah Grebing committed
40
41
42
43
44
45
46
47
48
49
50
51
<li> 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>

Alexander Weigl's avatar
Alexander Weigl committed
52
53
54
55
56

</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.
Sarah Grebing's avatar
Sarah Grebing committed
57

Alexander Weigl's avatar
Alexander Weigl committed
58
</p>
Sarah Grebing's avatar
Sarah Grebing committed
59
60
61
<h2>Publications</h2>
A full description of the language and debugging-concept is published at <a href="">HVC 2017</a>.

Alexander Weigl's avatar
Alexander Weigl committed
62
63
64
65
<h2>Features</h2>

<div class="column">
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
66
        <h3>Inspection of different parts of the proof state</h3>
67
        <p> 
Sarah Grebing's avatar
Sarah Grebing committed
68
69
70
71
72
73
74
        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>
        </p> 
Alexander Weigl's avatar
Alexander Weigl committed
75
76
    </div>
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
77
78
        <h3>Adjustable view on list of open goals</h3>
        <img src="img/simpleJavaGoalList.png" style="width:304px;height:228px;"  />
Alexander Weigl's avatar
Alexander Weigl committed
79
80
    </div>
    <div >
Sarah Grebing's avatar
Sarah Grebing committed
81
        <h3>Explore the proof tree of KeY</h3>
Alexander Weigl's avatar
Alexander Weigl committed
82
83
84
85
86
    </div>
</div>
<div style="clear: both;"/>
    <div class="column">
        <div >
Sarah Grebing's avatar
Sarah Grebing committed
87
            <h3>Stepwise evaluation of the proof script</h3>
Alexander Weigl's avatar
Alexander Weigl committed
88
            <p>
Sarah Grebing's avatar
Sarah Grebing committed
89
            The proof script can be evaluated stepwise and by running to a set breakpoint.
Alexander Weigl's avatar
Alexander Weigl committed
90
91
92
            </p>
        </div>
        <div >
Sarah Grebing's avatar
Sarah Grebing committed
93
94
            <h3>Set a breakpoint and run execution to breakpoint</h3>
             <img src="img/simpleJava2.png"  style="width:304px;height:228px;"/>
Alexander Weigl's avatar
Alexander Weigl committed
95
        </div>
Sarah Grebing's avatar
Sarah Grebing committed
96
97
98
        <div > 
            <h3> Step forward and step backward</h3>
            <img src="img/simpleJavaStep.png" style="width:304px;height:228px;" />
Alexander Weigl's avatar
Alexander Weigl committed
99
100
        </div>
    </div>
101
    <div style="clear: both;"/> 
Sarah Grebing's avatar
Sarah Grebing committed
102
103
    <p>
<footer style="border-top: #ccc 1px solid">
Alexander Weigl's avatar
Alexander Weigl committed
104
105
106
            Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
        </footer>
        </p>