spec/containers/deque.bend
bend-collections-laws-containers@1.0.0.0 · 194 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as E
4import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
5
6# Independent model: a deque is the finite sequence of its elements, front
7# first. Nothing here refers to the two-list representation.
8
9def item(-T: Data, x: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
10 match x:
11 case None{}:
12 Fail{E.EmptyDeque{}}
13 case Some{v}:
14 Done{v}
15
16def pop_front(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>:
17 match xs:
18 case Nil{}:
19 (Nil{}, E.OItem{Fail{E.EmptyDeque{}}})
20 case Con{h, t}:
21 (t, E.OItem{Done{h}})
22
23def pop_back(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>:
24 match xs:
25 case Nil{}:
26 (Nil{}, E.OItem{Fail{E.EmptyDeque{}}})
27 case Con{+h, +t}:
28 (C.init(T, Con{h, t}), E.OItem{item(T, C.last(T, Con{h, t}))})
29
30def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>:
31 match op:
32 case E.Length{}:
33 (xs, E.ONat{C.length(T, xs)})
34 case E.PushFront{x}:
35 (Con{x, xs}, E.OUnit{})
36 case E.PushBack{x}:
37 (C.snoc(T, xs, x), E.OUnit{})
38 case E.PopFront{}:
39 pop_front(T, xs)
40 case E.PopBack{}:
41 pop_back(T, xs)
42 case E.PeekFront{}:
43 (xs, E.OItem{item(T, C.head(T, xs))})
44 case E.PeekBack{}:
45 (xs, E.OItem{item(T, C.last(T, xs))})
46 case E.ToList{}:
47 (xs, E.OList{xs})
48
49def cons_obs(-T: Data, o: E.Obs<T>, r: List<&2, T> & List<&2, E.Obs<T>>) -> List<&2, T> & List<&2, E.Obs<T>>:
50 (m, os) = r
51 (m, Con{o, os})
52
53def run(-T: Data, ops: List<&2, E.Op<T>>, +xs: List<&2, T>) -> List<&2, T> & List<&2, E.Obs<T>>:
54 match ops:
55 case Nil{}:
56 (xs, Nil{})
57 case Con{+op, rest}:
58 cons_obs(T, Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op)), run(T, rest, Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))))
59
60# ---- contract (SPARK formal containers) ----
61# Each `<Subprogram>.<clause>` definition below states one Post clause of
62# that SPARK subprogram, as a proposition on this model; the table names the
63# clauses. proofs/containers/deque/ proves every clause under its clause name,
64# and its `impl` lemma carries them to the implementation.
65#
66# Contracts of the deque in the style of SPARK's formal vectors
67# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
68# 46ec319; model predicates in spec/lib/sequence.bend). The model is the
69# sequence front first. Each lemma is one Post clause of step; `impl`
70# (via P.step_ok) carries every clause to the implementation: DQ.step on
71# the deque of a shadow lands on the deque of a shadow whose model
72# satisfies it.
73#
74# SPARK subprogram (.ads line) ours clauses
75# Length (284) length length_result, length_frame
76# Empty_Vector (292) new new_empty, new_impl
77# Prepend (624) push_front push_front_length, push_front_first, push_front_shifted
78# Append (706) push_back push_back_length, push_back_prefix, push_back_element
79# Delete_First (825) pop_front pop_front_length, pop_front_shifted,
80# pop_front_result, pop_front_empty
81# Delete_Last (866) pop_back pop_back_length, pop_back_prefix,
82# pop_back_result, pop_back_empty
83# First_Element (913) peek_front peek_front_first, peek_front_frame, peek_front_empty
84# Last_Element (923) peek_back peek_back_last, peek_back_frame, peek_back_empty
85# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame
86# implementation DQ.step impl
87# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,
88# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,
89# Reference, Insert*, Prepend/Append with Count or a vector, Delete (at an
90# index or a count), Reverse_Elements, Swap, Find_Index, Reverse_Find_Index,
91# Contains, Has_Element. SPARK's Pre (not Is_Empty) is a defensive check:
92# on an empty deque pops and peeks return EmptyDeque and change nothing.
93
94def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>:
95 Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))
96
97def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>:
98 Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))
99
100# Length (284)
101def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
102 {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
103
104# Length (284)
105def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
106 {nx(T, xs, E.Length{}) == xs : List<&2, T>}
107
108# iteration (Iter_Model, 1193)
109def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
110 {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}
111
112# iteration (Iter_Model, 1193)
113def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
114 {nx(T, xs, E.ToList{}) == xs : List<&2, T>}
115
116# Prepend (624)
117def Prepend.push_front_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
118 {C.length(T, nx(T, xs, E.PushFront{v})) == 1n+C.length(T, xs) : Nat}
119
120# Prepend (624)
121def Prepend.push_front_first(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
122 {C.nth(T, nx(T, xs, E.PushFront{v}), 0n) == Some{v} : Maybe<&2, T>}
123
124# Prepend (624)
125def Prepend.push_front_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
126 V.RangeShifted(T, xs, nx(T, xs, E.PushFront{v}), 0n, C.length(T, xs), 1n)
127
128# Append (706)
129def Append.push_back_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
130 {C.length(T, nx(T, xs, E.PushBack{v})) == 1n+C.length(T, xs) : Nat}
131
132# Append (706)
133def Append.push_back_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
134 V.EqualPrefix(T, xs, nx(T, xs, E.PushBack{v}))
135
136# Append (706)
137def Append.push_back_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
138 {C.nth(T, nx(T, xs, E.PushBack{v}), C.length(T, xs)) == Some{v} : Maybe<&2, T>}
139
140# Delete_First (825)
141def Delete_First.pop_front_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
142 {1n+C.length(T, nx(T, Con{h, t}, E.PopFront{})) == C.length(T, Con{h, t}) : Nat}
143
144# Delete_First (825)
145def Delete_First.pop_front_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
146 V.RangeShifted(T, nx(T, Con{h, t}, E.PopFront{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.PopFront{})), 1n)
147
148# Delete_First (825)
149def Delete_First.pop_front_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
150 {ob(T, Con{h, t}, E.PopFront{}) == E.OItem{Done{h}} : E.Obs<T>}
151
152# Delete_First (825)
153def Delete_First.pop_front_empty(-T: Data) -> Type:
154 {step(T, Nil{}, E.PopFront{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}
155
156# Delete_Last (866)
157def Delete_Last.pop_back_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
158 {C.length(T, nx(T, Con{h, t}, E.PopBack{})) == C.length(T, t) : Nat}
159
160# Delete_Last (866)
161def Delete_Last.pop_back_prefix(-T: Data, +h: T, +t: List<&2, T>) -> Type:
162 V.EqualPrefix(T, nx(T, Con{h, t}, E.PopBack{}), Con{h, t})
163
164# Delete_Last (866)
165def Delete_Last.pop_back_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
166 {ob(T, Con{h, t}, E.PopBack{}) == E.OItem{item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
167
168# Delete_Last (866)
169def Delete_Last.pop_back_empty(-T: Data) -> Type:
170 {step(T, Nil{}, E.PopBack{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}
171
172# First_Element (913)
173def First_Element.peek_front_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
174 {ob(T, Con{h, t}, E.PeekFront{}) == E.OItem{Done{h}} : E.Obs<T>} & {C.nth(T, Con{h, t}, 0n) == Some{h} : Maybe<&2, T>}
175
176# First_Element (913)
177def First_Element.peek_front_frame(-T: Data, +xs: List<&2, T>) -> Type:
178 {nx(T, xs, E.PeekFront{}) == xs : List<&2, T>}
179
180# First_Element (913)
181def First_Element.peek_front_empty(-T: Data) -> Type:
182 {step(T, Nil{}, E.PeekFront{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}
183
184# Last_Element (923)
185def Last_Element.peek_back_last(-T: Data, +h: T, +t: List<&2, T>) -> Type:
186 {ob(T, Con{h, t}, E.PeekBack{}) == E.OItem{item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
187
188# Last_Element (923)
189def Last_Element.peek_back_frame(-T: Data, +xs: List<&2, T>) -> Type:
190 {nx(T, xs, E.PeekBack{}) == xs : List<&2, T>}
191
192# Last_Element (923)
193def Last_Element.peek_back_empty(-T: Data) -> Type:
194 {step(T, Nil{}, E.PeekBack{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}