To load a script it needs to be called in the main script.
 For example to load the script cpwob() type cpwob; in the body of the script main()
+ For this right click to the scripts declaration and select "Set as Mainscript".
+
+
+These example scripts are only for demonstration purposes,
+the underlying verification system just needs to be invoked with the automatic strategy "auto".
+This can be seen in the first script.
+
+The interactive script is to demonstrate the interactive rule applications.
\ No newline at end of file
diff git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/help.html b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/help.html
new file mode 100644
index 00000000..91766cfc
 /dev/null
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/help.html
@@ 0,0 +1,42 @@
+
+
+
Quicksort's split methods
+
This script is part of a case study to evaluate our language KPS. It is used to
+ prove the Split method of a Quicksort implementation.
+
This script is used to guide the proof for the method
+ split() of a Quicksort implementation.
+
In the first
+ lines the proof state is preprocessed, i.e., the program is symbolically.
+ The user is now left with a proof in which the proof goals each
+ correspond a program state and a part of the proof obligation that needs to be shown for this path.
+ For each of the more than 30 proof goals the next foreach block in the script invokes the
+ prover's strategy tryclose, which tries to close the proof goal with builtin strategies or,
+ if this is not successful, prunes the proof back to the goal the user has seen last.
+
+ In the two remaining proof goals, it needs to be shown that during the
+ loop execution the permutation property of the input array and the partial sorted array
+ is preserved and
+ that the loop invariant together with the rest of the program implies the post condition.
+ To show that the permutation property holds, we make use of the taclet seqPermFromSwap:
+ This taclet states that if we know that A is a permutation of B and we have to show that C is a permutation of D,
+ then it suffices to prove that
+
+
B is equal to D
+
and there exist two indices in A such that if the elements at these positions are swapped we obtain B.
+
+The two proof obligations to show are added to the sequents suceedent and after applying the rule andRight
+four proof goals remain: two where we have to show case (1) and two where we have to show case (2).
+
+
+
+
+
In the cases block, a distinction according to the shape of the proof
+ obligation introduced by the seqPermFromSwap taclet is done and those proof branches that
+ could be handled by the prover's auto strategy are captured by the first
+ case. In the second case the prover needs guidance in the form of quantifier
+ instantiations before it is able to find a proof.
+
+
+
+
+
\ No newline at end of file
diff git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html
index dd0476fa..d1bed190 100644
 a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro.html
@@ 1,92 +1,140 @@


 Introduction to Proof Scripting Language for the KeY system





Language Constructs
This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.

Proof scripts are textual representations of rule applications,
settings changes and macro invocations.


Proof Commands

Proof commands start with an identifier followed by optional
arguments:

command argName="argument" "argument without name" ;

Every command is terminated with a semicolon. There are named
arguments in the form argName="argument" and unnamed argument without
name. Single '...'and double quotes "..." can both be used.

Singleline comments are start with //.


KeY Rules/Taclets
All KeY rules can be used as proof command.
The following command structure is used to apply single KeY rules onto the sequent of a selected goal node.
If no argument is following the proof command the taclet corresponding to this command has to match at most once on the
sequent.
If more terms or formulas to which a proof command is applicable exist, arguments have to be
given that indicate the where to apply the rule to.

A rule command has the following syntax:
RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")? (maxSteps=INT)
 with:
+
Language Constructs
+
Proof scripts are textual representations of rule applications, settings changes
+ and strategy invocations (in the case of KeY as underlying verification
+ system also referred to as macros).
+
Variables and Types
+
We need to distinguish between: logic, program, and script variables.

TERM: specific subterm

TOP_LEVEL_FORMULA: specific top level formula

OCCURENCE_IN_SEQUENT: Number of occurence in the sequent

maxSteps: the number of steps KEY should at most use until it terminateds teh proof search
+
+
logic variable: Occur on sequents, bounded by a quantifier or in an update
+
+
+
program variable: declared and used in Java programs. They are constants
+ on the sequent.
+
+
+
script variable: declared and assignable within a script
+

If a rule has schema variables which must be instantiated manually,
such instantiations can be provided as arguments. A schema variable
named sv can be instantiated by setting the argument sv="..." or by
setting inst_sv="..." (the latter works also for conflict cases like
inst_occ="...").



Examples
+
Proof Script Language has script variables.
+
A script variable has a name, a type and a value.
+ Variables are declared by
+
var0:type;
+var1:type:=value;
+var2:=value;
+
+
+
+
+
Both statements declare a variable, in the latter case (var1 and var2) we directly assign a
+ value, in
+ the first form var0 receives a default value.
+
Types and Literals
+
We have following types: INT, TERM<Sort>, String.

andRight;

 Applicable iff there is only one matching spot on the sequent


eqSymm formula="a=b";

 This command changes the sequent "a=b ==> c=d" to "b=a ==> c=d"
 Using only "eqSymm;" alone would have been ambiguous.


eqSymm formula="a=b>c=d" occ=2;

 This command changes sequent "a=b>c=d ==>" to "a=b>d=c ==>".
 The occurrence number is needed since there are two possible applications on the formula


eqSymm formula="a=b>c=d" on="c=d";

 This command changes the sequent "a=b>c=d ==>" to "a=b>d=c ==>".
 It is simialr to the example above, but here the option to specify a
 subterm instead of an occurrence number is used.


cut cutFormula="x > y";

 This command is almost the same as 'cut "x>y"'

+
+
INT represents integer of arbitrary size.
+ 42
+ 134
+
+
+
TERM<S> represents a term of sort S in KeY.
+ S can be any sort given by KeY. If the sort is ommitied, then S=Any.
+

MacroCommands
In the KeY system macro commands are proof strategies tailored to specific proof tasks.
The available macro commands can be found using the command help.
Using them in a script is similar to using rule commands:

MACRONAME (PARAMETERS)?

Often used macro commands are:
+
`f(x)`
+ `g(a)`
+ `imp(p,q)`
+
+
STRING
+
+
"i am a string"
+
Special Variables
+
To expose settings of the underlying prover to the user we include special variables:
+
+
MAX_STEPS : amount denotes the maximum number of proof steps the underlying prover is allowed to
+ perform
+
+
+
Proof Commands
+
Proof commands start with an identifier followed by optional arguments:
Every command is terminated with a semicolon. There are named arguments in the
+ form argName=”argument” and unnamed argument without name. Single '...' and
+ double quotes "..." can both be used.
+
Singleline comments are start with //.
+
KeY Rules/Taclets
+
All KeY rules can be used as proof command. The following command structure is
+ used to apply single KeY rules onto the sequent of a selected goal node. If no
+ argument is following the proof command the taclet corresponding to this command
+ has to match at most once on the sequent.
+
If more terms or formulas to which a proof command is applicable exist,
+ arguments have to be given that indicate the where to apply the rule to.
OCCURENCE_IN_SEQUENT: Number of occurence in the sequent
+
maxSteps the number of steps KEY should at most use until it terminateds teh proof search
+
+
If a rule has schema variables which must be instantiated manually,
+ such instantiations can be provided as arguments. A schema variable
+ named sv can be instantiated by setting the argument sv=”…” or by
+ setting inst_sv=”…” (the latter works also for conflict cases like
+ inst_occ=”…”).
+
Examples
+
+
andRight;
+
+
Applicable iff there is only one matching spot on the sequent
+
+
+
eqSymm formula="a=b";
+
This command changes the sequent a=b ==> c=d to b=a ==> c=d Using only
+ eqSymm; alone would have been ambiguous.
+
+
+
eqSymm formula="a=b>c=d" occ=2;
+
This command changes sequent a=b>c=d ==> to a=b>d=c ==>. The
+ occurrence number is needed since there are two possible applications on the
+ formula
+
+
+
eqSymm formula="a=b>c=d" on="c=d";
+
This command changes the sequent “a=b>c=d ==>” to “a=b>d=c ==>”.
+ It is simialr to the example above, but here the option to specify a
+ subterm instead of an occurrence number is used.
+
+
+
cut cutFormula="x > y";
+
+
+
This command is almost the same as cut \x>y``
+
MacroCommands
+
In the KeY system macro commands are proof strategies tailored to specific proof tasks.
+ The available macro commands can be found using the command help.
+ Using them in a script is similar to using rule commands:
+
MACRONAME (PARAMETERS)?
+
Often used macro commands are:
symbex : performs symbolic execution
auto: invokes the automatic strategy of key
+
heap_simp: performs heap simplification
autopilot: full autopilot
autopilot_prep: preparation only autopilot
split_prop: propositional expansion w/ splits
@@ 96,9 +144,8 @@ Often used macro commands are:
Example:

auto;
+
Example:
+
auto;
Selectors
As nited before proof commands are implemented as single goal statements.
Some proof commands split a proof into more than one goal.
@@ 110,187 +157,13 @@ case MATCHER:
STATEMENTS
[default:
STATEMENTS]?
}

+}
Control Flow Statements
The script language allows different statements for controlflow.
ControlFlow statements define blocks, therefor it is neccessary to use curly braces after a controlflow statement.
+
+
The script language allows different statements for controlflow.
+ ControlFlow statements define blocks, therefor it is neccessary to use curly braces after a controlflow statement.
foreach {STATEMENTS}
theOnly {STATEMENTS}

repeat {STATEMENTS}







\ No newline at end of file
+
repeat {STATEMENTS}
+
\ No newline at end of file
diff git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro_old.html b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro_old.html
new file mode 100644
index 00000000..dd0476fa
 /dev/null
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/intro_old.html
@@ 0,0 +1,296 @@
+
+
+ Introduction to Proof Scripting Language for the KeY system
+
+
+
+
+
Language Constructs
+This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.
+
+Proof scripts are textual representations of rule applications,
+settings changes and macro invocations.
+
+
Proof Commands
+
+Proof commands start with an identifier followed by optional
+arguments:
+
+command argName="argument" "argument without name" ;
+
+Every command is terminated with a semicolon. There are named
+arguments in the form argName="argument" and unnamed argument without
+name. Single '...'and double quotes "..." can both be used.
+
+Singleline comments are start with //.
+
+
KeY Rules/Taclets
+All KeY rules can be used as proof command.
+The following command structure is used to apply single KeY rules onto the sequent of a selected goal node.
+If no argument is following the proof command the taclet corresponding to this command has to match at most once on the
+sequent.
+If more terms or formulas to which a proof command is applicable exist, arguments have to be
+given that indicate the where to apply the rule to.
+
+A rule command has the following syntax:
+RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")? (maxSteps=INT)
+ with:
+
+
TERM: specific subterm
+
TOP_LEVEL_FORMULA: specific top level formula
+
OCCURENCE_IN_SEQUENT: Number of occurence in the sequent
+
maxSteps: the number of steps KEY should at most use until it terminateds teh proof search
+
+
+If a rule has schema variables which must be instantiated manually,
+such instantiations can be provided as arguments. A schema variable
+named sv can be instantiated by setting the argument sv="..." or by
+setting inst_sv="..." (the latter works also for conflict cases like
+inst_occ="...").
+
+
+
Examples
+
+
andRight;
+
+ Applicable iff there is only one matching spot on the sequent
+
+
eqSymm formula="a=b";
+
+ This command changes the sequent "a=b ==> c=d" to "b=a ==> c=d"
+ Using only "eqSymm;" alone would have been ambiguous.
+
+
eqSymm formula="a=b>c=d" occ=2;
+
+ This command changes sequent "a=b>c=d ==>" to "a=b>d=c ==>".
+ The occurrence number is needed since there are two possible applications on the formula
+
+
eqSymm formula="a=b>c=d" on="c=d";
+
+ This command changes the sequent "a=b>c=d ==>" to "a=b>d=c ==>".
+ It is simialr to the example above, but here the option to specify a
+ subterm instead of an occurrence number is used.
+
+
cut cutFormula="x > y";
+
+ This command is almost the same as 'cut "x>y"'
+
+
+
MacroCommands
+In the KeY system macro commands are proof strategies tailored to specific proof tasks.
+The available macro commands can be found using the command help.
+Using them in a script is similar to using rule commands:
+
+MACRONAME (PARAMETERS)?
+
+Often used macro commands are:
+
+
symbex : performs symbolic execution
+
auto: invokes the automatic strategy of key
+
autopilot: full autopilot
+
autopilot_prep: preparation only autopilot
+
split_prop: propositional expansion w/ splits
+
nosplit_prop: propositional expansion w/o splits
+
simp_upd: update simplification
+
simp_heap: heap simplification
+
+
+
+Example:
+
+auto;
+
Selectors
+As nited before proof commands are implemented as single goal statements.
+Some proof commands split a proof into more than one goal.
+To allow to apply proof commands in proof state with more than one proof goal, the language allows for
+a selector statement cases. Such a casesstatement has the following structure:
+
+cases {
+case MATCHER:
+STATEMENTS
+[default:
+STATEMENTS]?
+}
+
+
Control Flow Statements
+The script language allows different statements for controlflow.
+ControlFlow statements define blocks, therefor it is neccessary to use curly braces after a controlflow statement.
+
+
foreach {STATEMENTS}
+
theOnly {STATEMENTS}
+
repeat {STATEMENTS}
+
+
+
+
+
+
+
\ No newline at end of file
diff git a/website/docs/index.md b/website/docs/index.md
index 2d5bd0ea..17103738 100644
 a/website/docs/index.md
+++ b/website/docs/index.md
@@ 75,18 +75,81 @@ is published at [HVC 2017](http://rdcu.be/E4fF)
## 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 loadthe statusbar indicates that the contract was loaded.
+
+### Setting a breakpoint and starting the Interpreter
The video will be uploaded on 23th, January.
+
+
+
+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.
+
+### 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 autogenerated matching expressions from the
+interactive rule applications.
+
+
+
## Features
@@ 128,7 +191,7 @@ Your browser does not support the video tag or WebM.
Stepwise script execution: step over and into.
Our special offers for time travellers: Go backwards in time
 and then Back to the Future,again!
+ and then Back to the Future, again!
@@ 145,8 +208,8 @@ Your browser does not support the video tag or WebM.
Downloads

PSDBG  Version 1.0FM will be available at 23th, January
 psdbg1.0fm.jar
+
PSDBG  Version 1.0FM
+ psdbg1.0fm.jar
Special Version for the tool paper at Formal Methods 2018.
Including examples and all dependencies.

2.24.1