Fix sortedness spec

KeYProject · Jun 15, 2024 · aac550f · aac550f
1 parent 226a2ce
commit aac550f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
@@ -82,7 +82,7 @@ private int binSearch(int v) {
 
     /*@ public normal_behaviour
       @  ensures \dl_seqPerm(\old(seq), seq);
-      @  ensures  (\forall int x,y; 0<=x<y<seq.length-1; (\bigint)seq[x] <= (\bigint)seq[y]);
+      @  ensures  (\forall int x,y; 0<=x<y<seq.length; (\bigint)seq[x] <= (\bigint)seq[y]);
       @  assignable footprint;
       @*/
     public void sort() {

diff --git a/startkey.sh b/startkey.sh