modernising the coupling invariant.

KeYProject · Apr 12, 2024 · f5a5cfc · f5a5cfc
1 parent 9121854
commit f5a5cfc
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
@@ -11,8 +11,7 @@ public class ArrayList implements List {
       @ private invariant 0 <= size && size <= array.length;
       @ private invariant (\forall int i; 0 <= i && i < size; array[i] != null);
       @
-      @ private invariant seq.length == size;
-      @ private invariant (\forall int i; 0 <= i && i < size; array[i] == (\bigint)seq[i]);
+      @ private invariant seq == \seq_sub(\array2seq(array), 0, size);
       @*/
 
     /*@ public normal_behaviour