Skip to content

Commit 079d161

Browse files
added arraydeque axioms
1 parent 709a559 commit 079d161

File tree

1 file changed

+20
-0
lines changed

1 file changed

+20
-0
lines changed

axioms/axioms.md

+20
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,26 @@ TreeSet
7272
* `contains(clear!(t), e) --> false`
7373
* `contains(add!(t, e1), e2) --> e2==e1 ? true : contains(t, e2)`
7474

75+
ArrayDeque
76+
=========
77+
* `size([]) --> 0`
78+
* `size(addLast!(d, e)) --> size(d)+1`
79+
* `size(addFirst!(d, e)) --> size(d)+1`
80+
* `size(removeFirst!(d)) --> size(d)-1`
81+
* `size(removeLast!(d)) --> size(d)-1`
82+
* `peekLast([]) --> null`
83+
* `peekLast(addLast!(d, e)) --> e`
84+
* `peekLast(addFirst!(d, e)) --> size(d)==0 ? e : peekLast(d)`
85+
* `peekLast(removeLast!(d, e)) --> peekLastCount(d, 0, 1)`
86+
* `peekLast(removeFirst!(d, e)) --> peekLastCount(d, 1, 0)`
87+
* `peekLastCount([], i, j) --> null`
88+
* `peekLastCount(addLast!(d, e), i, j) --> j>0 ? peekLastCount(d, i, j-1) : (i>0 ? (size(d)==i ? null : e) : e)`
89+
* `peekLastCount(addFirst!(d, e), i, j) --> size(d)==0 && i==0 && j==0 ? e : (i>0 ? peekLastCount(d, i-1, j) : (size(d)==j ? null : peekLastCount(d, i, j)))
90+
* `peekLastCount(removeFirst!(d), i , j) --> peekLastCount(d, i+1, j)`
91+
* `peekLastCount(removeLast!(d), i, j) --> peekLastCount(d, i, j+1)`
92+
93+
Note: peekFirst would be very similar to peekLast
94+
7595
File
7696
======
7797
* `read(filereader(file(f, d, l, n), p)) == d[p]`

0 commit comments

Comments
 (0)