Test added

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EnvironmentTest.java

@@ -113,8 +113,8 @@ public class EnvironmentTest {
 
     @Test
     public void testLoadQuickSortSplit() throws IOException, ParseException, ParserException {
-        File javaFile = new File(getFile(getClass(), "javaTestFiles/quicksort/Quicksort.java" ));
-        File scriptFile = new File(getFile(getClass(), "javaTestFiles/quicksort/script.kps" ));
+        File javaFile = new File(getFile(getClass(), "javaTestFiles/quicksort/split/Quicksort.java"));
+        File scriptFile = new File(getFile(getClass(), "javaTestFiles/quicksort/split/script.kps"));
         String contractName= "Quicksort[Quicksort::split([I,int,int)].JML normal_behavior operation contract";
 
         try {

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java

@@ -106,16 +106,30 @@ public class ExecuteTest {
 
     @Test
     public void testQuickSortSplit() throws IOException, ParseException, ParserException {
-        File keyFile = new File(getFile(getClass(), "javaTestFiles/quicksort/problem.key" ));
-        File scriptFile = new File(getFile(getClass(), "javaTestFiles/quicksort/script.kps" ));
+        File keyFile = new File(getFile(getClass(), "javaTestFiles/quicksort/split/problem.key"));
+        File scriptFile = new File(getFile(getClass(), "javaTestFiles/quicksort/split/script.kps"));
         String contractName= "Quicksort[Quicksort::split([I,int,int)].JML normal_behavior operation contract";
 
-        Execute exec = create(getFile(getClass(), "javaTestFiles/quicksort/problem.key" ),
-                "-s", getFile(getClass(), "javaTestFiles/quicksort/script.kps" ));
+        Execute exec = create(getFile(getClass(), "javaTestFiles/quicksort/split/problem.key"),
+                "-s", getFile(getClass(), "javaTestFiles/quicksort/split/script.kps"));
 
         Interpreter<KeyData> run = exec.run();
         Assert.assertTrue(run.getCurrentGoals().isEmpty());
         System.out.println("The proof of Quicksorts split method was closed");
     }
 
+    @Test
+    public void testQuickSortSort() throws IOException, ParseException, ParserException {
+        File keyFile = new File(getFile(getClass(), "javaTestFiles/quicksort/sort/problem.key"));
+        File scriptFile = new File(getFile(getClass(), "javaTestFiles/quicksort/sort/script.kps"));
+        String contractName = "Quicksort[Quicksort::sort([I,int,int)].JML normal_behavior operation contract";
+
+        Execute exec = create(getFile(getClass(), "javaTestFiles/quicksort/sort/problem.key"),
+                "-s", getFile(getClass(), "javaTestFiles/quicksort/sort/script.kps"));
+
+        Interpreter<KeyData> run = exec.run();
+        Assert.assertTrue(run.getCurrentGoals().isEmpty());
+        System.out.println("The proof of Quicksorts sort method was closed");
+    }
+
 }
\ No newline at end of file

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/sort/problem.key

+\profile "Java Profile";
+
+\settings {
+"#Proof-Settings-Config-File
+#Mon Jan 15 22:38:57 CET 2018
+[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
+[StrategyProperty]VBT_PHASE=VBT_SYM_EX
+[SMTSettings]useUninterpretedMultiplication=true
+[SMTSettings]SelectedTaclets=
+[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
+[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
+[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
+[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
+[SMTSettings]instantiateHierarchyAssumptions=true
+[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
+[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
+[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
+[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
+[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
+[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
+[Strategy]Timeout=-1
+[Strategy]MaximumNumberOfAutomaticApplications=10000
+[SMTSettings]integersMaximum=2147483645
+[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:allow , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off
+[SMTSettings]useConstantsForBigOrSmallIntegers=true
+[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
+[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
+[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
+[SMTSettings]maxGenericSorts=2
+[SMTSettings]integersMinimum=-2147483645
+[SMTSettings]invariantForall=false
+[SMTSettings]UseBuiltUniqueness=false
+[SMTSettings]explicitTypeHierarchy=false
+[Strategy]ActiveStrategy=JavaCardDLStrategy
+[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
+[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
+"
+}
+
+\javaSource "";
+
+\proofObligation "#Proof Obligation Settings
+#Mon Jan 15 22:38:57 CET 2018
+name=Quicksort[Quicksort\\:\\:sort([I,int,int)].JML normal_behavior operation contract.0
+contract=Quicksort[Quicksort\\:\\:sort([I,int,int)].JML normal_behavior operation contract.0
+class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
+";
\ No newline at end of file

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/sort/script.kps

+script sort() {
+	autopilot_prep;
+	
+	foreach{
+		simp_upd;
+		tryclose;
+	}
+	
+	seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)),length(array), any::select(heapAfter_split, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))))`;
+
+	seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_split, array, arr(u))))`;
+
+
+	seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort_0, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))))`;
+
+	seqPermTrans formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_split, array, arr(u))))`;
+
+	seqPermTrans formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort, array, arr(u))))`;
+
+	seqPermSym formula = `seqPerm(seqDef{int u;}(Z(0(#)), length(array), int::select(heap, array, arr(u))),
+         seqDef{int u;}(Z(0(#)), length(array), any::select(heapAfter_sort_0, array, arr(u))))`;
+
+	auto;
+}
\ No newline at end of file

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/split/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;
+
+    }
+}

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/split/proof-settings.props

+#Proof-Settings-Config-File
+#Mon Feb 05 16:31:07 CET 2018
+[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
+[StrategyProperty]VBT_PHASE=VBT_SYM_EX
+[SMTSettings]useUninterpretedMultiplication=true
+[SMTSettings]SelectedTaclets=
+[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
+[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
+[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
+[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
+[SMTSettings]instantiateHierarchyAssumptions=true
+[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
+[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
+[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
+[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
+[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
+[Strategy]Timeout=-1
+[Strategy]MaximumNumberOfAutomaticApplications=10000
+[SMTSettings]integersMaximum=2147483645
+[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , runtimeExceptions-runtimeExceptions\:allow , JavaCard-JavaCard\:off , Strings-Strings\:on , modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:on , reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off
+[SMTSettings]useConstantsForBigOrSmallIntegers=true
+[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
+[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
+[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
+[SMTSettings]maxGenericSorts=2
+[SMTSettings]integersMinimum=-2147483645
+[SMTSettings]invariantForall=false
+[SMTSettings]UseBuiltUniqueness=false
+[SMTSettings]explicitTypeHierarchy=false
+[Strategy]ActiveStrategy=JavaCardDLStrategy
+[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
+[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE