using Microsoft.Contracts; public class ArrayList : Collection { [Rep] private object[]! elements = new object[3]; // The Rep attribute lets object invarians depend on the state of the array private int siz = 0; invariant elements.Length > 0; invariant 0 <= siz && siz <= elements.Length; invariant elements.GetType() == typeof(object[]); [Pure] public int Size() ensures result == siz; { return siz; } [Pure] public bool LegalElement(object o) ensures result; { return true; } [Pure] public bool Contains(object o) ensures result == exists{int j in (0: siz); elements[j] == o}; { for(int i = 0; i < siz; i++) invariant !exists{int j in (0: i); elements[j] == o}; { if (elements[i] == o) return true; } return false; } public bool Add(object o) ensures result; { expose (this) { if (siz == elements.Length) { object[] tmp = new object[siz*2]; System.Array.Copy(elements, tmp, siz); elements = tmp; } elements[siz] = o; siz++; } assert elements[siz-1] == o; // needed to find instantiation for quantifier in postcondition of Contains return true; } }