Proof Script Debugger for the KeY System¶

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:

1. integration of domain specific entities like goal, formula, term and rule as first-class citizens into the language;
2. 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
3. a repetition construct which allows repeated application of proof strategies;
4. support for proof exploration within the language.

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.

Publications¶

A full description of the language and debugging-concept is published at HVC 2017. A short tool description is also available.

Debugging Script for Quicksort’s split method.¶

Selecting the proof script¶

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.

Please note that after a succesful load the statusbar indicates that the contract was loaded.

Setting a breakpoint and starting the Interpreter¶

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.

Stepping into, over and reverse and continue¶

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¶

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¶

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.

Features¶

Inspection of different parts of the proof state

The different parts of the proof state can be inspected:

• list of open goals
• sequent of selected open goal
• path through program (if existing) for selected open goal

Adjustable view on list of open goals

Explore the proof tree of KeY

Set a breakpoint and run execution to breakpoint

Mark lines with an (conditional) breakpoint to pause the script execution.

Stepwise evaluation for time travellers

Stepwise script execution: step over and into. Our special offers for time travellers: Go backwards in time and then Back to the Future, again!

Interactive Rule Application

Select rules for interactive application.

Usage Notes

Terms in KPS are enquoted using backticks `. Entering these in the editor of PDBG requires a keyboard layout with the option "no dead keys" enabled.

Downloads

• PSDBG - Experimental Version psdbg-1.2-experimental.jar
  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.
  One major change is the syntax for Matching Expressions. The wildcard symbol is now "?" instead of "_".
  Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
  License: GPLv3 Third Party Licenses
  Executable with java -jar psdbg-1.2-experimental.jar
• PSDBG - Version 1.0.2c-FM psdbg-1.0.2c-fm.jar
  First implementation of PSDBG, including examples.
  Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
  License: GPLv3 Third Party Licenses
  Executable with java -jar psdbg-1.0.2c-fm.jar

---