...

KeYProject · Apr 10, 2024 · 9121854 · 9121854
1 parent dca5411
commit 9121854
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
@@ -21,7 +21,7 @@ public class ArrayList implements List {
     public /*@ pure @*/ ArrayList() {
         this.array = new int[10];
         //@ set seq = \seq_empty;
-        //@ set footprint = \set_union(\all_fields(array), \all_fields(this));
+        //@ set footprint = \locset(array[*], this.*);
     }
 
     public int get(int index) {
@@ -37,8 +37,8 @@ public void add(int o) {
             array = Arrays.copyOf(array, array.length + 10);
         }
         array[size++] = o;
-        //@ set seq = \seq_concat(seq, \seq_singleton(o));
-        //@ set footprint = \set_union(\all_fields(array), \all_fields(this));
+        //@ set seq = seq + \seq(o);
+        //@ set footprint = \locset(array[*], this.*);
     }
 
     public int find(int value) {
@@ -125,7 +125,7 @@ private void swap(int a, int b) {
         int t = array[a];
         array[a] = array[b];
         array[b] = t;
-        //@ set seq = \seq_put(seq, a, array[a]);
-        //@ set seq = \seq_put(seq, b, array[b]);
+        //@ set seq = \seq_upd(seq, a, array[a]);
+        //@ set seq = \seq_upd(seq, b, array[b]);
     }
 }