README.md 1.75 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1 2
# PSDBG -- Proof Script Debugger 

alexander.weigl's avatar
alexander.weigl committed
3
![logo](share/logo.png)
sarah.grebing's avatar
sarah.grebing committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29

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:

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

# About this Repository

The latest build as jar file can be downloaded here. 
sarah.grebing's avatar
sarah.grebing committed
30 31 32 33 34 35 36 37 38
Please note that some funtionlities may not work in this jar as it is the build 
of the development version of PSDBG.

# Usage Notes

Terms in KPS are enquoted using backticks [`]. Entering these requires a 
keyboard layout with the option "no dead keys".
If this is not possible the terms can be entered by using the shortcut Ctrl+E 
which adds a pair of backticks to the cursor position.