From a64a5a0a337d6101bb165be7a411741169b06019 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Wed, 10 Jan 2018 16:48:11 +0100 Subject: [PATCH] Lulus Quicksort in own quicksort dir --- .../kit/iti/formal/psdbg/parser/ASTDiff.java | 5 + .../examples/java/quicksort/QuickSort.java | 23 ++++ .../psdbg/examples/lulu/LuLuQuickSort.java | 2 +- .../psdbg/gui/controller/DebuggerMain.java | 58 ++++----- .../edu.kit.iti.formal.psdbg.examples.Example | 1 + .../examples/java/quicksort/Quicksort.java | 110 ++++++++++++++++++ .../psdbg/examples/java/quicksort/script.kps | 47 ++++++++ 7 files changed, 219 insertions(+), 27 deletions(-) create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java create mode 100644 ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/Quicksort.java create mode 100644 ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java index dea2fc02..178d1b1b 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java @@ -148,6 +148,11 @@ public class ASTDiff extends DefaultASTVisitor { return null; } + /** + * @param old + * @param rev + * @return + */ public ProofScript diff(ProofScript old, ProofScript rev) { other = rev; return (ProofScript) visit(old); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java new file mode 100644 index 00000000..8bd8b0d8 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java @@ -0,0 +1,23 @@ +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")); + } + +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/LuLuQuickSort.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/LuLuQuickSort.java index 7993d913..a52fe43a 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/LuLuQuickSort.java +++ b/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")); } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index 71524a13..771323d7 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/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 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 diff --git a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example index 1a989c42..083208ea 100644 --- a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example +++ b/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 diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/Quicksort.java b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/Quicksort.java new file mode 100644 index 00000000..23d7bb6f --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/Quicksort.java @@ -0,0 +1,110 @@ +/** + * 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 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 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; + + } +} diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps new file mode 100644 index 00000000..d8d31d16 --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps @@ -0,0 +1,47 @@ +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 -- 2.26.2