From f5a5cfc450a8b7e88fa1d95604cdf5d6964509e8 Mon Sep 17 00:00:00 2001
From: Mattias Ulbrich <ulbrich@kit.edu>
Date: Fri, 12 Apr 2024 17:34:53 +0200
Subject: [PATCH] modernising the coupling invariant.

---
 ArrayList/src/ArrayList.java | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
index ae6dbaf..125fcde 100644
--- 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