1:
2: package mylist;
3:
4: public interface List {
5:
6: /**
7: * Returns the number of elements in the list.
8: *
9: * @pre true
10: * @post @nochange
11: */
12: public int size();
13:
14: /**
15: * Returns true if and only if the list is empty.
16: *
17: * @pre true
18: * @post @result <=> size() > 0
19: * @post @nochange
20: */
21: public boolean isEmpty();
22:
23: /**
24: * Returns the i-th element in the list.
25: *
26: * @pre i >= 0 && i < size()
27: * @post @nochange
28: */
29: public Object element(int i);
30:
31: /**
32: * Returns the first element in the list.
33: *
34: * @pre !isEmpty()
35: * @post @result == element(0)
36: * @post @nochange
37: */
38: public Object head();
39:
40: /**
41: * Returns the last element in the list.
42: *
43: * @pre !isEmpty()
44: * @post @result == element(size() - 1)
45: * @post @nochange
46: */
47: public Object last();
48:
49: /**
50: * Inserts a new element into the list at the i-th position.
51: *
52: * @pre item != null && i >= 0 && i <= size()
53: * @post size() == size()@pre + 1
54: * @post @forall k : [0 .. size() - 1] @
55: * (k < i ==> element(k)@pre == element(k)) &&
56: * (k == i ==> item@pre == element(k)) &&
57: * (k > i ==> element(k - 1)@pre == element(k)
58: */
59: public void insert(Object item, int i);
60:
61: /**
62: * Inserts a new element at the head of the list.
63: *
64: * @pre item != null
65: * @post size() == size()@pre + 1
66: * @post item@pre == element(0)
67: * @post @forall k : [1 .. size() - 1] @ element(k - 1)@pre == element(k)
68: */
69: public void insertHead(Object item);
70:
71: /**
72: * Inserts a new element at the end of the list.
73: *
74: * @pre item != null
75: * @post size() == size()@pre + 1
76: * @post item@pre == element(size() - 1)
77: * @post @forall k : [0 .. size() - 2] @ element(k)@pre == element(k)
78: */
79: public void insertLast(Object item);
80:
81: /**
82: * Remove the element at the i-th position.
83: *
84: * @pre size() > 0
85: * @pre i >= 0 && i < size()
86: * @post @result = element(i)@pre
87: * @post size() == size()@pre - 1
88: * @post @forall k : [0 .. size() - 1] @
89: * (k < i ==> element(k)@pre == element(k)) &&
90: * (k >= i ==> element(k + 1)@pre == element(k))
91: */
92: public Object remove(int i);
93:
94: /**
95: * Remove the element at the head.
96: *
97: * @pre size() > 0
98: * @post @result = element(0)@pre
99: * @post @forall k : [1 .. size() - 1] @ element(k + 1)@pre == element(k)
100: */
101: public Object removeHead();
102:
103: /**
104: * Remove the element at the end.
105: *
106: * @pre size() > 0
107: * @post @result = element(size() - 1)@pre
108: * @post @forall k : [0 .. size() - 1] @ element(k)@pre == element(k)
109: */
110: public Object removeLast();
111:
112: }