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 KeY. KeY is an interactive program verification system for Java program annotated with the Java Modeling Language (JML).
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:
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.
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
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.
Please note that after a succesful load the statusbar indicates that the contract was loaded.
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.
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.
In this video the successful proof is shown and it is demonstrated how to access the full proof tree of the proof for the
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.
Furthermore, we show how to use our SequentMatcher Window to enhance the auto-generated matching expressions from the interactive rule applications.
The different parts of the proof state can be inspected:
java -jar psdbg-1.2-experimental.jar
java -jar psdbg-1.0.2c-fm.jar