public class ArrayList { private Object[] elementData; private int size; /*: public specvar init :: bool; public specvar content :: "(int * obj) set"; public specvar csize :: int; public specvar msize :: int; vardefs "init == elementData ~= null" vardefs "content == {(i, n). 0 <= i & i < size & n = elementData.[i]}" vardefs "csize == size" vardefs "msize == elementData..Array.length" invariant InitInv: "~init --> size = 0 & elementData = null" invariant SizeInv: "init --> 0 <= size & size <= elementData..Array.length" invariant ElementDataInv: "init --> elementData : alloc & elementData : hidden" invariant HiddenInv: "hidden \<subseteq> alloc"; invariant NotHiddenInv: "init --> (ALL i. ((0 <= i & i < size) --> elementData.[i] ~: hidden))" invariant AllocInv: "init --> (ALL i. ((0 <= i & i < size) --> elementData.[i] : alloc))" invariant RangeInv1: "init --> (ALL i. 0 <= i & i < size --> (EX v. (i,v) : content))"; invariant RangeInv2: "init --> (ALL i v. (i,v) : content --> 0 <= i & i < size)"; invariant RangeInvInj: "init --> (ALL i v1 v2. (i,v1) : content & (i,v2) : content --> v1=v2)" invariant InjInv: "ALL x y. x ~= y & x..elementData ~= null --> x..elementData ~= y..elementData"; */ public ArrayList(int initialCapacity) /*: requires "~init & 0 < initialCapacity" modifies "this..init", "this..msize" ensures "init & content = {} & csize = 0 & msize = initialCapacity" */ { elementData = new /*: hidden */ Object[initialCapacity]; } public void trimToSize() /*: requires "init" modifies msize ensures "msize = csize" */ { int oldCapacity = elementData.length; if (size < oldCapacity) { Object oldData[] = elementData; elementData = new /*: hidden */ Object[size]; int i = 0; while /*: inv "0 <= i & (ALL j. (oldData.[j] = arrayRead (old Array.arrayState) (old elementData) j)) & (ALL j. (((0 <= j & j < i) --> elementData.[j] = oldData.[j]))) & (ALL a i. a ~= elementData --> arrayRead (old Array.arrayState) a i = a.[i])" */ (i < size) { elementData[i] = oldData[i]; i = i + 1; } } } public void ensureCapacity(int minCapacity) /*: requires "init" modifies msize ensures "minCapacity <= msize & old msize <= msize" */ { _ensureCapacity(minCapacity); } private void _ensureCapacity(int minCapacity) /*: requires "init & theinvs" modifies "Array.arrayState", elementData, msize, "ArrayList.hidden" ensures "minCapacity \<le> msize \<and> old msize \<le> msize \<and> (\<forall> x. x..init = (fieldRead (old ArrayList.init) x)) \<and> (\<forall> a j. a \<noteq> elementData \<longrightarrow> a.[j] = arrayRead (old arrayState) a j) \<and> (\<forall> j. ((0 \<le> j \<and> j < size) \<longrightarrow> elementData.[j] = arrayRead (old arrayState) (old elementData) j)) \<and> (\<forall> o1. (o1 \<in> old alloc) \<longrightarrow> ((o1 \<in> old hidden) = (o1 \<in> hidden))) \<and> theinvs" */ { int oldCapacity = elementData.length; if (minCapacity > oldCapacity) { Object oldData[] = elementData; int newCapacity = (oldCapacity * 3)/2 + 1; if (newCapacity < minCapacity) newCapacity = minCapacity; elementData = new /*: hidden */ Object[newCapacity]; int i = 0; while /*: inv "0 \<le> i \<and> (\<forall> j. ((0 \<le> j \<and> j < size \<longrightarrow> oldData.[j] = arrayRead (old arrayState) (old elementData) j))) \<and> (\<forall> j. ((0 \<le> j \<and> j < i) \<longrightarrow> elementData.[j] = oldData.[j])) \<and> (\<forall> a j. a \<noteq> elementData \<longrightarrow> a.[j] = arrayRead (old arrayState) a j)" */ (i < size) { elementData[i] = oldData[i]; i = i + 1; } } } public int size() /*: requires "init" ensures "result = csize" */ { return size; } public boolean isEmpty() /*: requires "init" ensures "result = (csize = 0)" */ { return size == 0; } public boolean contains(Object elem) /*: requires "init" ensures "(result = (EX i. (i, elem) : content))"; */ { int index = indexOfInt(elem); //: noteThat PosIndex: "0 <= index --> ((index,elem) : content)"; //: noteThat NegIndex: "index = -1 --> ~(EX i. (i,elem) : content)"; //: noteThat IndexLemma: "0 <= index | index = -1"; boolean res = (0 <= index); /*: note ResultLemma: "res = (EX i. (i, elem) : content)" from PosIndex, NegIndex, IndexLemma; */ return res; } public int indexOf(Object elem) /*: requires "init" ensures "-1 <= result & result < csize & (result ~= -1 --> (result, elem) : content) & (result ~= -1 --> ~(EX i. i < result & (i, elem) : content)) & (result = -1 --> ~(EX i. (i, elem) : content))" */ { return indexOfInt(elem); } private int indexOfInt(Object elem) /*: requires "init & theinvs" ensures "-1 <= result & result < csize & (result ~= -1 --> (result, elem) : content) & (result ~= -1 --> ~(EX i. i < result & (i, elem) : content)) & (result = -1 --> ~(EX i. (i, elem) : content)) & theinvs" */ { int i = 0; while /*: inv "0 <= i & (ALL j. 0 <= j & j < i --> elem ~= elementData.[j])" */ (i < size) { if (elementData[i] == elem) return i; i = i + 1; } return -1; } public int lastIndexOf(Object elem) /*: requires "init" ensures "-1 <= result & result < csize & (result ~= -1 --> ((result, elem) : content) & ~(EX i. result < i & (i, elem) : content)) & (result = -1 --> ~(EX i. (i, elem) : content))" */ { int i = size - 1; while /*: inv "i < size & (ALL j. i < j & j < size --> elem ~= elementData.[j]) & (ALL x i. ((x : alloc & x : Array & x ~: hidden) --> x.[i] = arrayRead (old Array.arrayState) (old x) i))" */ (i >= 0) { if (elementData[i] == elem) return i; i = i - 1; } return -1; } public Object[] toArray() /*: requires "init" modifies "new..arrayState" ensures "(ALL i e. (i, e) : content --> result.[i] = e) & (ALL i. 0 <= i & i < result..Array.length --> (i, result.[i]) : content)" */ { int i = 0; Object[] res = new Object[size]; while /*: inv "theinvs & comment ''C1'' (0 <= i) & comment ''C2'' (content = old content) & comment ''IA'' (ALL j. (0 <= j & j < i --> res.[j] = elementData.[j])) & comment ''IB'' (ALL x i. (x ~= res --> x.[i] = arrayRead (old Array.arrayState) x i)) & comment ''IC'' (ALL j. ((0 <= j & j < size) --> elementData.[j] ~: hidden)) & comment ''ID'' (ALL j. ((0 <= j & j < size) --> elementData.[j] : alloc))" */ (i < size) { res[i] = elementData[i]; i = i + 1; } return res; } public Object get(int index) /*: requires "init & 0 <= index & index < csize" ensures "(index, result) : content" */ { return elementData[index]; } public Object set(int index, Object element) /*: requires "init & 0 <= index & index < csize" modifies content ensures "(index, result) : old content & content = (old content - {(index, result)}) Un {(index, element)}" */ { Object oldValue = elementData[index]; elementData[index] = element; return oldValue; } private boolean add1(Object o) /*: requires "init & theinvs" modifies "Array.arrayState", elementData, msize, "ArrayList.hidden", content, size, csize ensures "(old csize, o) : content & comment ''addContentChange'' (ALL j. ((0 <= j & j < old csize) --> ((ALL e. (j, e) : content --> (j, e) : old content) & (ALL e. (j, e) : old content --> (j, e) : content)))) & comment ''csizeChange'' (csize = old csize + 1) & result & old msize <= msize & csize <= msize & (ALL a j. a ~: hidden --> a.[j] = arrayRead (old Array.arrayState) a j) & (ALL o1. (o1 : old alloc) --> ((o1 : old hidden) = (o1 : hidden))) & (ALL x. x..init = (fieldRead (old ArrayList.init) x)) & theinvs" */ { _ensureCapacity(size + 1); elementData[size] = o; size = size + 1; //: noteThat "old csize < size"; return true; } public boolean add(Object o) /*: requires "init" modifies content, csize, msize ensures "(old csize, o) : content & (ALL j. ((0 <= j & j < old csize) --> ((ALL e. (j, e) : content --> (j, e) : old content) & (ALL e. (j, e) : old content --> (j, e) : content)))) & csize = old csize + 1 & result & old msize <= msize & csize <= msize" */ { return add1(o); } public void add_at(int index, Object element) /*: requires "comment ''addAtPre'' (init & 0 <= index & index <= csize)" modifies content, csize, msize ensures "((index, element) : content) & (ALL j e. (0 <= j & j < index --> ((j, e) : content) = ((j, e) : old content)) & (index < j & j < csize --> ((j, e) : content) = ((j - 1, e) : old content))) & (csize = (old csize) + 1) & (msize >= (old msize)) & (csize <= msize)" */ { _ensureCapacity(size + 1); int i = size - 1; while /*: inv "index - 1 <= i & i <= size - 1 & (ALL a j. ((a ~: hidden) --> a.[j] = arrayRead (old Array.arrayState) a j)) & ((i = size - 1) --> (ALL j. ((0 <= j & j < size) --> elementData.[j] ~: hidden))) & ((i < size - 1) --> (ALL j. ((0 <= j & j < size + 1) --> elementData.[j] ~: hidden))) & ((i = size - 1) --> (ALL j. ((0 <= j & j < size) --> elementData.[j] : alloc))) & ((i < size - 1) --> (ALL j. ((0 <= j & j < size + 1) --> elementData.[j] : alloc))) & ((ALL j. ((0 <= j & j <= i) --> elementData.[j] = arrayRead (old Array.arrayState) (old elementData) j))) & ((ALL j. ((0 <= j & j <= index & j < size) --> elementData.[j] = arrayRead (old Array.arrayState) (old elementData) j))) & ((ALL j. ((i < j & j < size) --> elementData.[j + 1] = arrayRead (old Array.arrayState) (old elementData) j))) & (ALL x i. (x ~= elementData & x ~= (old elementData)) --> (x.[i] = (arrayRead (old Array.arrayState) (old x) i)))" */ (index <= i) { elementData[i + 1] = elementData[i]; i = i - 1; } elementData[index] = element; size = size + 1; /*: noteThat InvMeans: "(ALL j. ((0 <= j & j < index & j < (old size)) --> elementData.[j] = arrayRead (old Array.arrayState) (old elementData) j)) & (ALL j. ((index <= j & j < (old size)) --> elementData.[j + 1] = arrayRead (old Array.arrayState) (old elementData) j))"; */ //: noteThat IndexRange: "0 <= index & index <= old size"; //: noteThat CsizeIsSize: "csize = size"; /*: noteThat PostCond: "(ALL j e. (0 <= j & j < index --> ((j, e) : content) = ((j, e) : old content)) & (index < j & j < csize --> ((j, e) : content) = ((j - 1, e) : old content)))" from InvMeans, PostCond, content_def, IndexRange, CsizeIsSize; */ /*: noteThat OtherPostCond: "(index, element) : content" from OtherPostCond, content_def, IndexRange; */ } public Object remove_at(int index) /*: requires "init & 0 <= index & index < csize" modifies content, csize ensures "(ALL j e. (0 <= j & j < index --> ((j, e) : content) = ((j, e) : old content)) & (index <= j & j < csize --> ((j, e) : content) = ((j + 1, e) : old content))) & ((index, result) : old content) & (csize = old csize - 1)"; */ { Object oldValue = elementData[index]; shift(index); return oldValue; } public Object remove_at_dep(int index) /*: requires "init & 0 <= index & index < csize" modifies content, csize ensures "((index, result) : old content) & (csize = old csize - 1) & (ALL j e. ((0 <= j & j < index) --> ((j, e) : content) = ((j, e) : old content)) & ((index <= j & j < csize) --> ((j, e) : content) = ((j + 1, e) : old content)))" */ { Object oldValue = elementData[index]; int i = index; while /*: inv "index <= i & (ALL j. ((0 <= j & j < index) --> elementData.[j] = (arrayRead (old Array.arrayState) (old elementData) j))) & (ALL j. ((index <= j & j < i) --> elementData.[j] = (arrayRead (old Array.arrayState) elementData (j + 1)))) & (ALL j. ((i <= j & j < size) --> elementData.[j] = (arrayRead (old Array.arrayState) (old elementData) j))) & (ALL x i. x ~= elementData --> x.[i] = arrayRead (old Array.arrayState) (old x) i)" */ (i < size - 1) { elementData[i] = elementData[i+1]; i = i + 1; } size = size - 1; elementData[size] = null; return oldValue; } public boolean remove(Object o1) /*: requires "init" modifies content, csize ensures "((\<exists> i. (i, o1) \<in> old content) \<longrightarrow> (result \<and> (\<exists> i. ((i, o1) \<in> old content) \<and> \<not>(\<exists> j. j < i \<and> (j, o1) \<in> old content) \<and> (\<forall> j e. ((0 \<le> j \<and> j < i) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((i \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content))))))) \<and> (\<not>(\<exists> i. (i, o1) \<in> old content) \<longrightarrow> (\<not>result \<and> (content = old content)))" */ { int index = 0; while /*: inv "0 \<le> index \<and> theinvs \<and> alloc = old alloc \<and> (\<forall> j. 0 \<le> j \<and> j < index \<longrightarrow> o1 \<noteq> elementData.[j]) \<and> (\<forall> a i. a.[i] = old (a.[i])) \<and> comment ''ContentLoop'' (\<forall> x. x..content = old (x..content)) \<and> (\<forall> x. x..size = old (x..size))" */ (index < size) { if (elementData[index] == o1) { shift(index); /*: noteThat ThisContent: "\<forall> j e. ((0 \<le> j \<and> j < index) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((index \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content)))" from shift_Postcondition, ContentLoop; */ /*: witness "index" for PostconditionClause1: "(\<exists> i. (((i, o1) \<in> old content) \<and> \<not>(\<exists> j. j < i \<and> (j, o1) \<in> old content) \<and> (\<forall> j e. ((0 \<le> j \<and> j < i) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((i \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content))))))"; */ /*: note PostconditionClause2: "(\<not>(\<exists> i. (i, o1) \<in> old content) \<longrightarrow> (\<not>True \<and> (content = old content)))" from PostconditionClause1; */ return true; } index = index + 1; } return false; } public boolean remove2(Object o1) /*: requires "init" modifies content, csize ensures "(result --> (\<exists> i. ((i, o1) \<in> old content) \<and> \<not>(\<exists> j. j < i \<and> (j, o1) \<in> old content) \<and> (\<forall> j e. ((0 \<le> j \<and> j < i) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((i \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content)))))) \<and> (~result --> (\<not>(\<exists> i. (i, o1) \<in> old content) \<and> (content = old content)))" */ { int index = 0; while /*: inv "0 \<le> index \<and> theinvs \<and> alloc = old alloc \<and> (\<forall> j. 0 \<le> j \<and> j < index \<longrightarrow> o1 \<noteq> elementData.[j]) \<and> (\<forall> a i. a.[i] = old (a.[i])) \<and> (\<forall> x. x..content = old (x..content)) \<and> (\<forall> x. x..size = old (x..size))" */ (index < size) { if (elementData[index] == o1) { shift(index); /*: noteThat ThisContent: "\<forall> j e. ((0 \<le> j \<and> j < index) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((index \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content)))" from shift_Postcondition, LoopInv */ /*: witness "index" for PostconditionClause1: "(\<exists> i. (((i, o1) \<in> old content) \<and> \<not>(\<exists> j. j < i \<and> (j, o1) \<in> old content) \<and> (\<forall> j e. ((0 \<le> j \<and> j < i) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((i \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content))))))"; */ return true; } index = index + 1; } return false; } private void shift(int index) /*: requires "init & 0 <= index & index < size & theinvs" modifies "Array.arrayState", size, content, csize ensures "(ALL j. ((0 <= j & j < index) --> elementData.[j] = arrayRead (old Array.arrayState) (old elementData) j)) & (ALL j. ((index <= j & j < size) --> elementData.[j] = arrayRead (old Array.arrayState) (old elementData) (j + 1))) & elementData.[size] = null & (ALL a i. a ~= elementData --> a.[i] = arrayRead (old Array.arrayState) (old a) i) & (size = old size - 1) & (\<forall> x. x \<noteq> this \<longrightarrow> x..content = old (x..content)) \<and> (\<forall> j e. ((0 \<le> j \<and> j < index) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((index \<le> j \<and> j < csize) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content)))) \<and> theinvs" */ { int i = index; while /*: inv "index <= i \<and> (ALL j. ((0 <= j & j < index) --> elementData.[j] = (arrayRead (old Array.arrayState) (old elementData) j))) & (ALL j. ((index <= j & j < i) --> elementData.[j] = (arrayRead (old Array.arrayState) (old elementData) (j + 1)))) & (ALL j. ((i <= j & j < size) --> elementData.[j] = (arrayRead (old Array.arrayState) (old elementData) j))) & (ALL a i. ((a ~= elementData) --> a.[i] = arrayRead (old Array.arrayState) (old a) i)) \<and> (\<forall> j e. ((0 \<le> j \<and> j < index) \<longrightarrow> (((j, e) \<in> content) = ((j, e) \<in> old content))) \<and> ((index \<le> j \<and> j < i) \<longrightarrow> (((j, e) \<in> content) = ((j + 1, e) \<in> old content))))" */ (i < size - 1) { elementData[i] = elementData[i+1]; i = i + 1; } size = size - 1; elementData[size] = null; } public void clear() /*: requires "init" modifies content, csize ensures "content = {} & csize = 0" */ { int i = 0; while /*: inv "0 <= i & (ALL x i. x \<noteq> elementData \<longrightarrow> x.[i] = arrayRead (old Array.arrayState) (old x) i) & (ALL x. x : Object.alloc & x : ArrayList & x..init & x ~= this --> (ALL i. ((0 <= i & i < x..size) --> x..elementData.[i] ~: hidden))) & (ALL x. x : Object.alloc & x : ArrayList & x..init & x ~= this --> (ALL i. ((0 <= i & i < x..size) --> x..elementData.[i] : alloc)))" */ (i < size) { elementData[i] = null; i = i + 1; } size = 0; } // Two stack operations public void pushLast(Object element) /*: requires "init" modifies content, csize, msize ensures "comment ''sizeInc'' (csize = old csize + 1) & comment ''contentAdd'' (content = old content Un {(csize - 1,element)})" */ { boolean res = add1(element); //: noteThat inserted: "(csize - 1, element) : content"; { //: pickAny i::int, e::obj {//: assuming h1: "(i,e) : old content"; //: noteThat g1: "0 <= i & i < old csize"; //: noteThat g2: "(i,e) : content" from g2,g1, addContentChange, h1; } //: noteThat thus1: "(i,e) : old content --> (i,e) : content"; {//: assuming hh1: "(i,e) : content"; //: noteThat gg1: "0 <= i & i < csize"; //: noteThat gg2: "i = csize - 1 --> (i,e) : old content Un {(csize - 1,element)}"; {//: assuming hh2: "i < csize - 1"; //: noteThat gg3: "(i,e) : old content" from addContentChange, hh2, gg1, hh1, csize_def, csizeChange; } //: noteThat possible: "i < csize - 1 | i = csize - 1"; //: noteThat gg4: "(i,e) : old content Un {(csize - 1,element)}" from gg1, gg3, gg2, g2, h1, csize_def, csizeChange, possible; } /*: noteThat pointwise: "((i,e) : old content --> (i,e) : content) & ((i,e) = (csize - 1, element) --> (i,e) : content) & ((i,e) : content --> (i,e) : (old content Un {(csize - 1,element)}))" forSuch i,e; */ } //: noteThat tpost: "(content = old content Un {(csize - 1,element)})" from pointwise; //: note ContentFrame: "ALL al. al : old alloc & al : ArrayList & al ~: hidden & al ~= this --> al..content = old (al..content)" from add1_Postcondition; } public Object popLast() /*: requires "init & csize > 0" modifies content, csize ensures "csize = old csize - 1 & content = old content - {(csize,result)}" */ { size = size - 1; Object res = elementData[size]; elementData[size] = null; return res; } }