diff --git a/contract-order.txt b/contract-order.txt index f4f088d..3b7e734 100644 --- a/contract-order.txt +++ b/contract-order.txt @@ -109,6 +109,7 @@ de.wiesler.Partition[de.wiesler.Partition::bucketCountsToTotalCount([I,int,int,[ de.wiesler.SampleParameters[de.wiesler.SampleParameters::isValidForLen(int)].JML model_behavior operation contract.0 +de.wiesler.Sorter[de.wiesler.Sorter::seqUpd(\seq,int,int)].JML model_behavior operation contract.0 de.wiesler.Sorter[de.wiesler.Sorter::allBucketsInRangeSorted([I,int,int,[I,int,int,int)].JML model_behavior operation contract.0 de.wiesler.Sorter[de.wiesler.Sorter::allBucketsPartitioned([I,int,int,[I,int)].JML model_behavior operation contract.0 de.wiesler.Sorter[de.wiesler.Sorter::allBucketsPartitionedLemma(de.wiesler.Classifier,[I,int,int,[I)].JML model_behavior operation contract.0 diff --git a/src/main/java/de/wiesler/Sorter.java b/src/main/java/de/wiesler/Sorter.java index cc9baf6..14c665a 100644 --- a/src/main/java/de/wiesler/Sorter.java +++ b/src/main/java/de/wiesler/Sorter.java @@ -572,7 +572,8 @@ public static void fallback_sort(int[] values, int begin, int end) { @ requires 0 <= idx < seq.length; @ ensures (\forall int x; 0 <= x < seq.length; @ \result[x] == (x == idx ? value : seq[x])); - @ static model \seq seqUpd(\seq seq, int idx, int value) { + @ ensures \result.length == seq.length; + @ static no_state model \seq seqUpd(\seq seq, int idx, int value) { @ return \seq_concat(\seq_concat( @ \seq_sub(seq, 0, idx), @ \seq_singleton(value)), @@ -596,11 +597,11 @@ public static void insertion_sort(int[] values, int begin, int end) { /*@ loop_invariant \dl_seqPerm(\dl_seq_def_workaround(begin, end, values), @ \old(\dl_seq_def_workaround(begin, end, values))); @ loop_invariant begin < k <= end; + @ loop_invariant (\forall int x; k <= x < end; values[x] == \old(values[x])); @ loop_invariant Functions.isSortedSlice(values, begin, k); @ assignable values[begin..end - 1]; @ decreases end - k; - */ - + @*/ for (; k < end; ++k) { int value = values[k]; int hole = k; @@ -612,7 +613,7 @@ public static void insertion_sort(int[] values, int begin, int end) { @ loop_invariant i == k - 1 || Functions.isSortedSlice(values, begin, k+1); @ loop_invariant Functions.isSortedSlice(values, begin, k); @ loop_invariant \dl_seqPerm( - @ seqUpd(\dl_seq_def_workaround(begin, end, values), hole, value), + @ seqUpd(\dl_seq_def_workaround(begin, end, values), hole - begin, value), @ \old(\dl_seq_def_workaround(begin, end, values))); @ loop_invariant value <= values[hole]; @ assignable values[begin..k]; @@ -624,11 +625,11 @@ public static void insertion_sort(int[] values, int begin, int end) { // assert hole == i + 1 : i + " vs " + hole; //@ ghost \seq before; // This assume statement is harmless! - //@ assume before == seqUpd(\dl_seq_def_workaround(begin, end, values), hole, value); + //@ assume before == seqUpd(\dl_seq_def_workaround(begin, end, values), hole-begin, value); values[hole] = values[i]; - /*@ assert seqUpd(\dl_seq_def_workaround(begin, end, values), hole, value) == - @ \dl_seqSwap(before, i, hole); + /*@ assert seqUpd(\dl_seq_def_workaround(begin, end, values), i-begin, value) == + @ \dl_seqSwap(before, i-begin, hole-begin); @*/ hole = i; diff --git a/src/main/java/de/wiesler/notes.tmp b/src/main/java/de/wiesler/notes.tmp index f340c6b..1695e56 100644 --- a/src/main/java/de/wiesler/notes.tmp +++ b/src/main/java/de/wiesler/notes.tmp @@ -29,4 +29,15 @@ cut: sp(swap(before, i, hole), before) 1 2 4 4 5 3 ^ hole - ^ i \ No newline at end of file + ^ i + + ^ hole + ^ i + +1 2 4 3 5 + + + +upd(S, hole, value) + +