Commit db44f34a authored by Alexander Weigl's avatar Alexander Weigl 🐼
Browse files

Merge branch 'masterToMerge' into 'master'

Master to merge

See merge request !8
parents a4d6ca6e a7a05d05
Pipeline #17466 failed with stages
......@@ -188,9 +188,13 @@ public class Utils {
expContent.setMaxWidth(Double.MAX_VALUE);
expContent.add(label, 0, 0);
expContent.add(textArea, 0, 1);
alert.setWidth(400);
alert.setHeight(400);
alert.getDialogPane().setExpandableContent(expContent);
alert.setHeight(600);
alert.setWidth(400);
alert.showAndWait();
}
......@@ -247,6 +251,9 @@ public class Utils {
alert.setTitle("Proof Closed");
alert.setHeaderText("The proof is closed");
alert.setContentText("The proof using " + scriptName + " is closed");
alert.setWidth(400);
alert.setHeight(400);
/*StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw);
......
......@@ -45,13 +45,18 @@ public class WelcomePaneFMEdition extends AnchorPane {
* Load a test example
* @param event
*/
public void loadJavaTest(ActionEvent event) {
public void loadQuicksort(ActionEvent event) {
proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null);
Examples.loadExamples().forEach(example -> {
if (example.getName().equals("Quicksort example")) {
example.open(proofScriptDebugger);
}
});
}
/**
* Load teh help page documentation
* Load the help page documentation
* @param event
*/
public void loadHelpPage(ActionEvent event) {
......
......@@ -2,4 +2,24 @@
# Script commands to be used in proof scripts
#
de.uka.ilkd.key.macros.scripts.MacroCommand
de.uka.ilkd.key.macros.scripts.FocusOnSelectionAndHideCommand
de.uka.ilkd.key.macros.scripts.AutoCommand
de.uka.ilkd.key.macros.scripts.CutCommand
de.uka.ilkd.key.macros.scripts.SetCommand
de.uka.ilkd.key.macros.scripts.SMTCommand
de.uka.ilkd.key.macros.scripts.RuleCommand
de.uka.ilkd.key.macros.scripts.LeaveCommand
de.uka.ilkd.key.macros.scripts.TryCloseCommand
de.uka.ilkd.key.macros.scripts.ExitCommand
de.uka.ilkd.key.macros.scripts.InstantiateCommand
de.uka.ilkd.key.macros.scripts.SelectCommand
de.uka.ilkd.key.macros.scripts.ScriptCommand
de.uka.ilkd.key.macros.scripts.LetCommand
de.uka.ilkd.key.macros.scripts.SchemaVarCommand
de.uka.ilkd.key.macros.scripts.JavascriptCommand
de.uka.ilkd.key.macros.scripts.SkipCommand
de.uka.ilkd.key.macros.scripts.AssumeCommand
de.uka.ilkd.key.macros.scripts.SettingsCommand
#de.uka.ilkd.key.macros.scripts.FinishSymbolicExecutionMacro
\ No newline at end of file
......@@ -9,4 +9,4 @@ edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample
edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList
edu.kit.iti.formal.psdbg.examples.lulu.LuLuQuickSort
edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax
edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax
\ No newline at end of file
......@@ -18,7 +18,7 @@
<h3>Thanks to:</h3>
<ul>
<li>Lulu Luang</li>
<li>An Thuy Tien Luong</li>
<li>Mattias Ulbrich</li>
</ul>
</body>
......
......@@ -12,4 +12,5 @@ Authors:
* Alexander Weigl <weigl@ira.uka.de>
https://formal.iti.kit.edu/~weigl
* Lulu Lulong
* An Thuy Tien Luong
......@@ -2,7 +2,14 @@
<body>
<h1>Contraposition</h1>
<p>To load a script it needs to be called in the main script.
For example to load the script cpwob() type <i>cpwob;</i> in the body of the script <i> main()</i></p>
For this right click to the scripts declaration and select "Set as Mainscript".
</p>
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.
</body>
</html>
\ No newline at end of file
......@@ -9,6 +9,7 @@ script interactive(){
impRight;
impRight;
impLeft;
}
script interactive_with_match(){
......
......@@ -12,25 +12,3 @@ script main() {
close;
}
script main1() {
impRight;
//instantiate var=`x` with=`c`;
//allLeft formula=`\forall` with=`a`;
//allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
}
script proj() {
impRight;
eqSymm formula = `f(c) = f(f(f(c)))`;
instantiate var=`x` with=`f(f(c))`;
//allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`f(f(c))`;
allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
//applyEqRigid;
//applyEq formula=`f(f(f(c))) = f(c)` occ=`f(f(c))`;
//applyEq formula=`f(f(f(c))) = f(c)` occ=4;
applyEq on=`f(f(c))` formula=`f(f(f(c))) = f(c)` ;
close;
//close formula=`f(f(c))=f(c)`;
}
\ No newline at end of file
<html>
<body>
<h1>Quicksort's split methods</h1>
<p>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.</p>
<p> This script is used to guide the proof for the method
split() of a Quicksort implementation.</p>
<p>In the first
lines the proof state is pre-processed, 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 built-in 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
<ol>
<li>B is equal to D</li>
<li>and there exist two indices in A such that if the elements at these positions are swapped we obtain B.</li>
</ol>
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).
</p>
<p> 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.
</p>
</body>
</html>
\ No newline at end of file
......@@ -14,8 +14,8 @@ script split_from_quicksort() {
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
auto;
case match `==> (\exists ?X (\exists ?Y _))`:
instantiate var=`?X`[?X \ X] with=`i_0`;
instantiate var=`?Y`[?Y \ Y] with=`j_0`;
instantiate var=X with=`i_0`;
instantiate var=Y with=`j_0`;
auto;
}
}
......
public class Test{
public class Simple{
......@@ -6,12 +6,12 @@ public class Test{
@ requires x >= 0;
@ ensures \result >0;
@*/
public int foo(int x){
public int very_simple(int x){
if(x > 0){
x--;
}else{
x++;
}
return x++;
return ++x;
}
}
\ No newline at end of file
......@@ -3,7 +3,10 @@
<head>
<meta charset="UTF-8">
<title>Java Simple Test Example</title>
This is a simple Java example.
<h1>Very Simple Java Example</h1>
This is a very simple Java example.
Please select the contract <em>Simple:very_simple</em> from the contract list.
</head>
<body>
......
script t1(){
symbex;
cases{
case match `?X >= 0,?X > 0 ==>`:
cut `?X = 0`[?X \ X];
foreach{
auto;
}
foreach{
tryclose;
}
}
......@@ -7,18 +7,23 @@
<?import javafx.scene.text.Font?>
<fx:root prefHeight="485.0" prefWidth="716.0" type="AnchorPane" xmlns="http://javafx.com/javafx/8.0.121"
xmlns:fx="http://javafx.com/fxml/1">
<children>
<Label layoutX="14.0" layoutY="14.0" text="Welcome to the ProofScriptDebugger">
<font>
<Font size="24.0"/>
</font>
</Label>
<Label text="FM 2018 - Edition">
<font>
<Font size="20.0"/>
</font>
</Label>
<padding>
<Insets top="25" right="25" bottom="25" left="25"/>
</padding>
<children>
<VBox>
<Label layoutX="14.0" layoutY="14.0" text="Welcome to the ProofScriptDebugger">
<font>
<Font size="24.0"/>
</font>
</Label>
<Label text="FM 2018 - Edition">
<font>
<Font size="20.0"/>
</font>
</Label>
</VBox>
<Label alignment="TOP_LEFT" layoutX="14.0" layoutY="71.0" prefHeight="129.0" prefWidth="573.0"
text="This application is the Proof Script debugger for the KeY system. It allows to perform proofs using a proof scripting language on top of the KeY system."
wrapText="true"/>
......@@ -99,8 +104,10 @@
</Button>
<!-- <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308"
onAction="#loadJavaTest" text="Java Test Example" GridPane.columnIndex="1" GridPane.rowIndex="1">
<Button contentDisplay="TOP" maxHeight="1.7976931348623157E308"
maxWidth="1.7976931348623157E308"
onAction="#loadQuicksort" text="Quicksort Example" GridPane.columnIndex="1"
GridPane.rowIndex="1">
<graphic>
<MaterialDesignIconView glyphName="NEW_BOX" size="24" />
</graphic>
......@@ -113,7 +120,7 @@
<MaterialDesignIconView glyphName="NEW_BOX" size="24" />
</graphic>
</Button>
-->
</children>
<StackPane.margin>
<Insets bottom="10.0" left="10.0" right="10.0" top="10.0"/>
......
<html>
<head>
<title>Introduction to Proof Scripting Language for the KeY system</title>
<meta content="">
<style></style>
</head>
<body>
<h1>Language Constructs</h1>
This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.
<br>
Proof scripts are textual representations of rule applications,
settings changes and macro invocations.
<h2>Proof Commands</h2>
Proof commands start with an identifier followed by optional
arguments:
<br>
command argName="argument" "argument without name" ;
<br>
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.
<br>
Single-line comments are start with //.
<h3>KeY Rules/Taclets</h3>
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.
<br>
A rule command has the following syntax:<br>
RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")? (maxSteps=INT)
<br>with:
<h1 id="language_constructs">Language Constructs</h1>
<p>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).</p>
<h2 id="variables_and_types">Variables and Types</h2>
<p>We need to distinguish between: logic, program, and script variables.</p>
<ul>
<li>TERM: specific sub-term</li>
<li>TOP_LEVEL_FORMULA: specific top level formula</li>
<li>OCCURENCE_IN_SEQUENT: Number of occurence in the sequent</li>
<li>maxSteps: the number of steps KEY should at most use until it terminateds teh proof search</li>
<li>
<p><strong>logic variable</strong>: Occur on sequents, bounded by a quantifier or in an update</p>
</li>
<li>
<p><strong>program variable</strong>: declared and used in Java programs. They are constants
on the sequent.</p>
</li>
<li>
<p><strong>script variable</strong>: declared and assignable within a script</p>
</li>
</ul>
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="...").
<h4>Examples</h4>
<p>Proof Script Language has script variables.</p>
<p>A script variable has a name, a type and a value.
Variables are declared by</p>
<div class="codehilite"><pre><span class="n">var0</span> <span class="o">:</span> <span class="n">type</span><span
class="o">;</span>
<span class="n">var1</span> <span class="o">:</span> <span class="n">type</span> <span class="o">:=</span> <span
class="n">value</span><span class="o">;</span>
<span class="n">var2</span> <span class="o">:=</span> <span class="n">value</span><span class="o">;</span>
</pre>
</div>
<p>Both statements declare a variable, in the latter case (<code>var1</code> and <code>var2</code>) we directly assign a
value, in
the first form <code>var0</code> receives a default value.</p>
<h3 id="types_and_literals">Types and Literals</h3>
<p>We have following types: <code>INT</code>, <code>TERM&lt;Sort&gt;</code>, <code>String</code>.</p>
<ul>
<li>andRight;</li>
<br>
Applicable iff there is only one matching spot on the sequent
<li>eqSymm formula="a=b";</li>
<br>
This command changes the sequent "a=b ==> c=d" to "b=a ==> c=d"
Using only "eqSymm;" alone would have been ambiguous.
<li>eqSymm formula="a=b->c=d" occ=2;</li>
<br>
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
<li>eqSymm formula="a=b->c=d" on="c=d";</li>
<br>
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.
<li>cut cutFormula="x > y";</li>
<br>
This command is almost the same as 'cut "x>y"'
<li>
<p><code>INT</code> represents integer of arbitrary size.
<code>42
-134</code></p>
</li>
<li>
<p><code>TERM&lt;S&gt;</code> represents a term of sort <code>S</code> in KeY.
<code>S</code> can be any sort given by KeY. If the sort is ommitied, then <code>S=Any</code>.</p>
</li>
</ul>
<h3>Macro-Commands</h3>
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:
<br>
MACRONAME (PARAMETERS)?
<br>
Often used macro commands are:
<p><code>`f(x)`
`g(a)`
`imp(p,q)`</code></p>
<ul>
<li><code>STRING</code></li>
</ul>
<p><code>"i am a string"</code></p>
<h3 id="special_variables">Special Variables</h3>
<p>To expose settings of the underlying prover to the user we include special variables:</p>
<ul>
<li><code>MAX_STEPS</code> : amount denotes the maximum number of proof steps the underlying prover is allowed to
perform
</li>
</ul>
<h2 id="proof_commands">Proof Commands</h2>
<p>Proof commands start with an identifier followed by optional arguments:</p>
<div class="codehilite"><pre>command argName=&quot;argument&quot; &quot;positional argument&quot; ;
</pre>
</div>
<p>Every command is terminated with a semicolon. There are named arguments in the
form argName=&rdquo;argument&rdquo; and unnamed argument without name. Single <code>'...'</code> and
double quotes <code>"..."</code> can both be used.</p>
<p>Single-line comments are start with <code>//</code>.</p>
<h2 id="key_rulestaclets">KeY Rules/Taclets</h2>
<p>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.</p>
<p>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.</p>
<p>A rule command has the following syntax:</p>
<div class="codehilite"><pre>RULENAME [on=TERM]?
[formula=TERM]
[occ=INT]
[inst_*=TERM]
</pre>
</div>
<p>with:</p>
<ul>
<li><code>TERM</code> specific sub-term</li>
<li><code>TOP_LEVEL_FORMULA</code>: specific top level formula</li>
<li><code>OCCURENCE_IN_SEQUENT</code>: Number of occurence in the sequent</li>
<li><code>maxSteps</code> the number of steps KEY should at most use until it terminateds teh proof search</li>
</ul>
<p>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=&rdquo;&hellip;&rdquo; or by
setting inst_sv=&rdquo;&hellip;&rdquo; (the latter works also for conflict cases like
inst_occ=&rdquo;&hellip;&rdquo;).</p>
<h3 id="examples">Examples</h3>
<ul>
<li><code>andRight;</code></li>
</ul>
<p>Applicable iff there is only one matching spot on the sequent</p>
<ul>
<li>
<p><code>eqSymm formula="a=b";</code></p>
<p>This command changes the sequent <code>a=b ==&gt; c=d</code> to <code>b=a ==&gt; c=d</code> Using only
<code>eqSymm;</code> alone would have been ambiguous.</p>
</li>
<li>
<p><code>eqSymm formula="a=b-&gt;c=d" occ=2;</code></p>
<p>This command changes sequent <code>a=b-&gt;c=d ==&gt;</code> to <code>a=b-&gt;d=c ==&gt;</code>. The
occurrence number is needed since there are two possible applications on the
formula</p>
</li>
<li>
<p><code>eqSymm formula="a=b-&gt;c=d" on="c=d";</code></p>
<p>This command changes the sequent &ldquo;a=b-&gt;c=d ==&gt;&rdquo; to &ldquo;a=b-&gt;d=c ==&gt;&rdquo;.
It is simialr to the example above, but here the option to specify a
subterm instead of an occurrence number is used.</p>
</li>
<li>
<p><code>cut cutFormula="x &gt; y";</code></p>
</li>
</ul>
<p>This command is almost the same as <code>cut \</code>x&gt;y``</p>
<h3 id="macro-commands">Macro-Commands</h3>
<p>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:</p>
<p><code>MACRONAME (PARAMETERS)?</code></p>
<p>Often used macro commands are:</p>
<ul>
<li>symbex : performs symbolic execution</li>
<li>auto: invokes the automatic strategy of key</li>
<li>heap_simp: performs heap simplification</li>
<li>autopilot: full autopilot</li>
<li>autopilot_prep: preparation only autopilot</li>
<li>split_prop: propositional expansion w/ splits</li>
......@@ -96,9 +144,8 @@ Often used macro commands are:
</ul>
Example:
auto;
<p>Example:</p>
<p>auto;
<h2>Selectors</h2>
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: <br>
STATEMENTS <br>
[default: <br>
STATEMENTS]?<br>
}
}</p>
<h2>Control Flow Statements</h2>
The script language allows different statements for control-flow.
Control-Flow statements define blocks, therefor it is neccessary to use curly braces after a control-flow statement.
<p>The script language allows different statements for control-flow.
Control-Flow statements define blocks, therefor it is neccessary to use curly braces after a control-flow statement.
<ul>
<li>foreach {STATEMENTS}</li>
<li>theOnly {STATEMENTS}</li>
<li>repeat {STATEMENTS}</li>
</ul>
<!--
Commands in scripts
-------------------
This list of available script commands is subject to change and to
extension. If you write your own script commands (s. below), please
addCell an explanation to this list here. The list is sorted alphabetically.
-- auto ------------------
Apply the automatic KeY strategy on the current goal. Optinally you
can specify the number of steps to run.
Examples:
auto steps=30000;
# run at most 30000 steps automatically.
-- cut -------------------
Performs a cut and thus splits the sequent into two goals. The unnamed
argument is the formula to cut with
Examples:
cut "value1 = value2";
-- exit ------------------
Terminate the script prematurely at that point. Used mainly for debug