More spec and verification of base case

KeYProject · Oct 24, 2023 · df5b888 · df5b888
1 parent d34107e
commit df5b888
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 8 deletions.
diff --git 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
@@ -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
@@ -29,4 +29,15 @@ cut: sp(swap(before, i, hole), before)
 1 2 4 4 5
     3
       ^ hole
-    ^ i
+    ^ i
+
+    ^ hole
+  ^ i
+
+1 2 4 3 5
+
+
+
+upd(S, hole, value)
+
+
-Original file line number
+Diff line change
@@ Expand Up / @@ -29,4 +29,15 @@ cut: sp(swap(before, i, hole), before) @@
 2 4 4 5
           ^ hole
-        ^ i
+        ^ i
+        ^ hole
+      ^ i
+2 4 3 5
+    upd(S, hole, value)