Lulus Quicksort in own quicksort dir

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java

@@ -148,6 +148,11 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
         return null;
     }
 
+    /**
+     * @param old
+     * @param rev
+     * @return
+     */
     public ProofScript diff(ProofScript old, ProofScript rev) {
         other = rev;
         return (ProofScript) visit(old);

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java

+package edu.kit.iti.formal.psdbg.examples.java.quicksort;
+
+import edu.kit.iti.formal.psdbg.examples.JavaExample;
+
+public class QuickSort extends JavaExample {
+
+    public QuickSort() {
+
+
+        setName("Quicksort example");
+
+        setHelpText(null);
+
+        setJavaFile(getClass().
+
+                getResource("Quicksort.java"));
+
+        setScriptFile(getClass().
+
+                getResource("script.kps"));
+    }
+
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/LuLuQuickSort.java

@@ -6,7 +6,7 @@ public class LuLuQuickSort extends JavaExample {
     public LuLuQuickSort() {
         setName("LuLu QuickSort");
         setHelpText(null);
-        setJavaFile(getClass().getResource("QuickSort.java"));
+        setJavaFile(getClass().getResource("Quicksort.java"));
         setScriptFile(getClass().getResource("QuickSort.kps"));
     }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -396,39 +396,18 @@ public class DebuggerMain implements Initializable {
         executeScript(false);
     }
 
-    @FXML
-    public void abortExecution() {
-        if (model.getDebuggerFramework() != null) {
-            try {
-                // try to friendly
-                Future future = executorService.submit(() -> {
-                    model.getDebuggerFramework().stop();
-                    model.getDebuggerFramework().unregister();
-                    model.getDebuggerFramework().release();
-                });
-
-                // wait a second!
-                future.get(1, TimeUnit.SECONDS);
-                // ungently stop
-                model.getDebuggerFramework().hardStop();
-            } catch (InterruptedException | ExecutionException | TimeoutException e) {
-                e.printStackTrace();
-            } finally {
-                model.setDebuggerFramework(null);
-            }
-        } else {
-            LOGGER.info("no interpreter running");
-        }
-    }
-
     private void executeScript(boolean addInitBreakpoint) {
         if (model.getDebuggerFramework() != null) {
-            Alert alert = new Alert(Alert.AlertType.CONFIRMATION, "Interpreter is already running \nDo want to abort it?",
+            Alert alert = new Alert(Alert.AlertType.CONFIRMATION, "Interpreter is already running \nDo you want to abort it?",
                     ButtonType.CANCEL, ButtonType.YES);
             Optional<ButtonType> ans = alert.showAndWait();
             ans.ifPresent(a -> {
                 if (a == ButtonType.OK) abortExecution();
             });
+
+            if (ans.isPresent() && ans.get() == ButtonType.CANCEL) {
+                return;
+            }
         }
 
         assert model.getDebuggerFramework() == null : "There should not be any interpreter running.";
@@ -454,6 +433,33 @@ public class DebuggerMain implements Initializable {
         executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
     }
 
+    @FXML
+    public void abortExecution() {
+
+        if (model.getDebuggerFramework() != null) {
+            try {
+                // try to friendly
+                Future future = executorService.submit(() -> {
+                    model.getDebuggerFramework().stop();
+                    model.getDebuggerFramework().unregister();
+                    model.getDebuggerFramework().release();
+                });
+
+                // wait a second!
+                future.get(1, TimeUnit.SECONDS);
+                // ungently stop
+                model.getDebuggerFramework().hardStop();
+
+            } catch (InterruptedException | ExecutionException | TimeoutException e) {
+                e.printStackTrace();
+            } finally {
+                model.setDebuggerFramework(null);
+            }
+        } else {
+            LOGGER.info("no interpreter running");
+        }
+    }
+
 
     /**
      * Execute the script that with using the interpreter that is build using the interpreterbuilder

ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example

@@ -3,6 +3,7 @@ edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
 edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
 edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
 edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
+edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort
 edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
 edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
 edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/Quicksort.java

+/**
+ * This example formalizes and verifies the wellknown quicksort
+ * algorithm for int-arrays algorithm.  It shows that the array
+ * is sorted in  the end and that it contains  a permutation of
+ * the original input.
+ *
+ * The   proofs   for   the  main   method   sort(int[])   runs
+ * automatically   while   the   other  two   methods   require
+ * interaction.  You   can  load   the  files   "sort.key"  and
+ * "split.key"  from the  example's  directory  to execute  the
+ * according proof scripts.
+ *
+ * The permutation property requires some interaction: The idea
+ * is that the only actual modification on the array are swaps
+ * within the "split" method. The sort method body contains
+ * three method invocations which each maintain the permutation
+ * property. By a repeated appeal to the transitivity of the
+ * permutation property, the entire algorithm can be proved to
+ * only permute the array.
+ *
+ * To establish  monotonicity, the key  is to specify  that the
+ * currently  handled block  contains  only  numbers which  are
+ * between   the    two   pivot   values    array[from-1]   and
+ * array[to]. The first  and last block are exempt  from one of
+ * these  conditions  since  they have  only  one  neighbouring
+ * block.
+ *
+ * The  example has  been  added  to show  the  power of  proof
+ * scripts.
+ *
+ * @author Mattias Ulbrich, 2015
+ */
+
+class Quicksort {
+
+    /*@ public normal_behaviour
+      @  ensures \dl_seqPerm(\dl_array2seq(array), \old(\dl_array2seq(array)));
+      @  ensures (\forall int i; 0<=i && i<array.length-1; array[i] <= array[i+1]);
+      @  assignable array[*];
+      @*/
+    public void sort(int[] array) {
+        if(array.length > 0) {
+            sort(array, 0, array.length-1);
+        }
+    }
+
+    /*@ public normal_behaviour
+      @  requires 0 <= from;
+      @  requires to < array.length;
+      @  requires from > 0 ==> (\forall int x; from<=x && x<=to; array[x] > array[from-1]);
+      @  requires to < array.length-1 ==> (\forall int x; from<=x && x<=to; array[x] <= array[to+1]);
+      @  ensures \dl_seqPerm(\dl_array2seq(array), \old(\dl_array2seq(array)));
+      @  ensures (\forall int i; from<=i && i<to; array[i] <= array[i+1]);
+      @  ensures from > 0 ==> (\forall int x; from<=x && x<=to; array[x] > array[from-1]);
+      @  ensures to < array.length-1 ==> (\forall int x; from<=x && x<=to; array[x] <= array[to+1]);
+      @  assignable array[from..to];
+      @  measured_by to - from + 1;
+      @*/
+    private void sort(int[] array, int from, int to) {
+        if(from < to) {
+            int splitPoint = split(array, from, to);
+            sort(array, from, splitPoint-1);
+            sort(array, splitPoint+1, to);
+        }
+    }
+
+    /*@ public normal_behaviour
+      @  requires 0 <= from && from < to && to <= array.length-1;
+      @  requires from > 0 ==> (\forall int x; from<=x && x<=to; array[from-1] < array[x]);
+      @  requires to < array.length-1 ==> (\forall int y; from<=y && y<=to; array[y] <= array[to+1]);
+      @  ensures \dl_seqPerm(\dl_array2seq(array), \old(\dl_array2seq(array)));
+      @  ensures from <= \result && \result <= to;
+      @  ensures (\forall int m; from <= m && m <= \result; array[m] <= array[\result]);
+      @  ensures (\forall int n; \result < n && n <= to; array[n] > array[\result]);
+      @  ensures from > 0 ==> (\forall int x; from<=x && x<=to; array[from-1] < array[x]);
+      @  ensures to < array.length-1 ==> (\forall int y; from<=y && y<=to; array[y] <= array[to+1]);
+      @  assignable array[from..to];
+      @*/
+    private int split(int[] array, int from, int to) {
+
+        int i = from;
+        int pivot = array[to];
+
+        /*@
+          @ loop_invariant from <= i && i <= j;
+          @ loop_invariant from <= j && j <= to;
+          @ loop_invariant \dl_seqPerm(\dl_array2seq(array), \old(\dl_array2seq(array)));
+          @ loop_invariant (\forall int k; from <= k && k < i; array[k] <= pivot);
+          @ loop_invariant (\forall int l; i <= l && l < j; array[l] > pivot);
+          @ loop_invariant from > 0 ==> (\forall int x; from<=x && x<=to; array[from-1] < array[x]);
+          @ loop_invariant to < array.length-1 ==> (\forall int y; from<=y && y<=to; array[y] <= array[to+1]);
+          @ decreases to + to - j - i + 2;
+          @ assignable array[from..to-1];
+          @*/
+        for(int j = from; j < to; j++) {
+            if(array[j] <= pivot) {
+                int t = array[i];
+                array[i] = array[j];
+                array[j] = t;
+                i++;
+            }
+        }
+
+        array[to] = array[i];
+        array[i] = pivot;
+
+        return i;
+
+    }
+}

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps

+script qs() {
+autopilot_prep;
+foreach{
+	tryclose;
+}
+
+cases{
+	default:
+		simp_upd;  //only 2nd open goal needs this
+		seqPermFromSwap;
+		andRight;
+}
+
+
+cases{
+	case match '#0.*':
+		auto;
+	case match '#1.*':
+				instantiate  var=`iv` with=`i_0`;
+				instantiate  var=`jv` with=`j_0`;
+				auto;
+}
+}
+
+
+
+script quicksort() {
+  autopilot_prep;
+  foreach{
+    tryclose;
+  }
+  foreach{
+    simp_upd;
+    seqPermFromSwap;
+    andRight;
+  }
+
+
+  cases{
+    case match '#0.*': //hier sollten bessere branchnamen hin
+        auto;
+    case match '#1.*': //hier sollten bessere branchnamen hin
+        instantiate  var=`iv` with=`i_0`;
+        instantiate  var=`jv` with=`j_0`;
+        auto;
+  }
+}
\ No newline at end of file