Proof for the base case

KeYProject · Oct 25, 2023 · a1e230f · a1e230f
1 parent df5b888
commit a1e230f
Show file tree

Hide file tree

Showing 2 changed files with 47,326 additions and 1 deletion.
diff --git a/src/main/java/de/wiesler/Sorter.java b/src/main/java/de/wiesler/Sorter.java
@@ -628,7 +628,7 @@ public static void insertion_sort(int[] values, int begin, int end) {
                 //@ 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), i-begin, value) ==
+                /* @ assert seqUpd(\dl_seq_def_workaround(begin, end, values), i-begin, value) ==
                   @   \dl_seqSwap(before, i-begin, hole-begin);
                   @*/