From ed20e7d0d8fa937d927491d9186bd260f970a589 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Wed, 27 Feb 2019 10:39:31 +0100 Subject: [PATCH] Added quisort as test case in case we want to change java versions --- .../psdbg/interpreter/EnvironmentTest.java | 35 +++++- .../formal/psdbg/interpreter/ExecuteTest.java | 13 +++ .../javaTestFiles/quicksort/Quicksort.java | 110 ++++++++++++++++++ .../javaTestFiles/quicksort/problem.key | 16 +++ .../quicksort/proof-settings.props | 36 ++++++ .../javaTestFiles/quicksort/script.kps | 24 ++++ .../psdbg/examples/java/quicksort/script.kps | 4 - 7 files changed, 228 insertions(+), 10 deletions(-) create mode 100644 rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/Quicksort.java create mode 100644 rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/problem.key create mode 100644 rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/proof-settings.props create mode 100644 rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/script.kps diff --git a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EnvironmentTest.java b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EnvironmentTest.java index 9ac2e0bf..d9bc4cda 100644 --- a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EnvironmentTest.java +++ b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/EnvironmentTest.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.api.ProofManagementApi; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.op.IObserverFunction; +import de.uka.ilkd.key.parser.ParserException; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -16,10 +17,13 @@ import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.util.KeYTypeUtil; import de.uka.ilkd.key.util.MiscTools; import static edu.kit.iti.formal.psdbg.TestHelper.getFile; +import org.apache.commons.cli.ParseException; +import org.junit.Assert; import org.junit.Test; import org.key_project.util.collection.ImmutableSet; import java.io.File; +import java.io.IOException; import java.net.URL; import java.util.HashMap; import java.util.LinkedList; @@ -88,12 +92,6 @@ public class EnvironmentTest { @Test public void bigInt2() { File location = new File(getFile(getClass(), "javaTestFiles/BigInteger.java")); - - - List classPaths = null; // Optionally: Additional specifications for API classes - File bootClassPath = null; // Optionally: Different default specifications for Java API - List includes = null; // Optionally: Additional includes to consider - try { KeYProofFacade facade = new KeYProofFacade(); // ProofApi proofApi = facade.loadKeyFile(location); @@ -113,4 +111,29 @@ 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" )); + String contractName= "Quicksort[Quicksort::split([I,int,int)].JML normal_behavior operation contract"; + + try { + KeYProofFacade facade = new KeYProofFacade(); + ProofManagementApi pma = KeYApi.loadFromKeyFile(javaFile); + facade.setEnvironment(pma.getCurrentEnv()); + List proofContracts = pma.getProofContracts(); + Contract chosen = null; + for (Contract c : proofContracts) { + if(c.getTypeName().equals(contractName)){ + chosen = c; + } + } + Assert.assertNotNull("We were able to find the contract", chosen); + + + } catch (ProblemLoaderException e) { + e.printStackTrace(); + } + } + } diff --git a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java index 8c305423..aa43bd37 100644 --- a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java +++ b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java @@ -104,4 +104,17 @@ public class ExecuteTest { System.out.println(currentState); } + @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" )); + 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" )); + + Interpreter run = exec.run(); + Assert.assertTrue(run.getCurrentGoals().isEmpty()); + } + } \ No newline at end of file diff --git a/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/Quicksort.java b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/Quicksort.java new file mode 100644 index 00000000..23d7bb6f --- /dev/null +++ b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/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/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/problem.key b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/problem.key new file mode 100644 index 00000000..39a51373 --- /dev/null +++ b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/problem.key @@ -0,0 +1,16 @@ +// This file is part of KeY - Integrated Deductive Software Design +// +// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany +// Universitaet Koblenz-Landau, Germany +// Chalmers University of Technology, Sweden +// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany +// Technical University Darmstadt, Germany +// Chalmers University of Technology, Sweden +// +// The KeY system is protected by the GNU General +// Public License. See LICENSE.TXT for details. +// + +\javaSource "./"; + +\chooseContract "Quicksort[Quicksort::split([I,int,int)].JML normal_behavior operation contract.0"; diff --git a/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/proof-settings.props b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/proof-settings.props new file mode 100644 index 00000000..79e300af --- /dev/null +++ b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/proof-settings.props @@ -0,0 +1,36 @@ +#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 diff --git a/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/script.kps b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/script.kps new file mode 100644 index 00000000..5eb96e09 --- /dev/null +++ b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/javaTestFiles/quicksort/script.kps @@ -0,0 +1,24 @@ +script split_from_quicksort() { + autopilot_prep; + foreach{ + tryclose; + } + foreach{ + simp_upd; + seqPermFromSwap; + andRight; + } + + +cases{ + case match `? ==> seqDef{?;}(?,?,?) = seqDef{?;}(?, ?, ?)`: + __KEY_MAX_STEPS:=10000; + auto; + case match `? ==> (\exists ?X:int; (\exists ?Y:int; ?))`: + instantiate var=X with=`i_0`; + instantiate var=Y with=`j_0`; + __KEY_MAX_STEPS:=60000; + auto; + } +} + 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 index 4a23df32..5eb96e09 100644 --- 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 @@ -1,7 +1,3 @@ -script test() { - autopilot_prep; -} - script split_from_quicksort() { autopilot_prep; foreach{ -- GitLab