Commit ed20e7d0 authored by Sarah Grebing's avatar Sarah Grebing

Added quisort as test case in case we want to change java versions

parent f5e20a42
Pipeline #41930 passed with stages
in 3 minutes and 40 seconds
......@@ -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<File> classPaths = null; // Optionally: Additional specifications for API classes
File bootClassPath = null; // Optionally: Different default specifications for Java API
List<File> 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<Contract> 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();
}
}
}
......@@ -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<KeyData> run = exec.run();
Assert.assertTrue(run.getCurrentGoals().isEmpty());
}
}
\ No newline at end of file
/**
* 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;
}
}
// 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";
#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
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;
}
}
script test() {
autopilot_prep;
}
script split_from_quicksort() {
autopilot_prep;
foreach{
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment