spec/containers/binary_heap.bend
bend-collections-laws-containers@1.0.0.0 · 215 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/binary_heap.bend as E
4import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
5
6# Independent model: a priority queue is the finite multiset of its elements,
7# represented canonically as the list sorted ascending by the comparator
8# (insertion sort). Equal-comparing elements are identical under the order
9# laws, so the sorted list is unique for each multiset. Nothing here refers
10# to trees.
11
12def le(~A: Data, ~cmp: A -> A -> Cmp, x: A, y: A) -> Bool:
13 Cmp.is_le(cmp(x, y))
14
15# Insert into a sorted list, before the first element not smaller than x.
16def ins(~A: Data, ~cmp: A -> A -> Cmp, +x: A, xs: List<&2, A>) -> List<&2, A>:
17 match xs:
18 case Nil{}:
19 Con{x, Nil{}}
20 case Con{+h, +t}:
21 Bool.pick(List<&2, A>, le(~A, ~cmp, x, h), Con{x, Con{h, t}}, Con{h, ins(~A, ~cmp, x, t)})
22
23# The multiset of a list, left to right.
24def from_list(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>, acc: List<&2, A>) -> List<&2, A>:
25 match xs:
26 case Nil{}:
27 acc
28 case Con{x, t}:
29 from_list(~A, ~cmp, t, ins(~A, ~cmp, x, acc))
30
31def item(-A: Data, x: Maybe<&2, A>) -> Result<&2, &2, E.Error, A>:
32 match x:
33 case None{}:
34 Fail{E.EmptyHeap{}}
35 case Some{v}:
36 Done{v}
37
38def pop(-A: Data, xs: List<&2, A>) -> List<&2, A> & E.Obs<A>:
39 match xs:
40 case Nil{}:
41 (Nil{}, E.OItem{Fail{E.EmptyHeap{}}})
42 case Con{h, t}:
43 (t, E.OItem{Done{h}})
44
45def step(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, op: E.Op<A>) -> List<&2, A> & E.Obs<A>:
46 match op:
47 case E.Length{}:
48 (xs, E.ONat{C.length(A, xs)})
49 case E.Push{x}:
50 (ins(~A, ~cmp, x, xs), E.OUnit{})
51 case E.Peek{}:
52 (xs, E.OItem{item(A, C.head(A, xs))})
53 case E.Pop{}:
54 pop(A, xs)
55 case E.FromList{ys}:
56 (from_list(~A, ~cmp, ys, Nil{}), E.OUnit{})
57 case E.ToSortedList{}:
58 (xs, E.OList{xs})
59
60def cons_obs(-A: Data, o: E.Obs<A>, r: List<&2, A> & List<&2, E.Obs<A>>) -> List<&2, A> & List<&2, E.Obs<A>>:
61 (m, os) = r
62 (m, Con{o, os})
63
64def run(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, +xs: List<&2, A>) -> List<&2, A> & List<&2, E.Obs<A>>:
65 match ops:
66 case Nil{}:
67 (xs, Nil{})
68 case Con{+op, rest}:
69 cons_obs(A, Pair.snd(List<&2, A>, E.Obs<A>, step(~A, ~cmp, xs, op)), run(~A, ~cmp, rest, Pair.fst(List<&2, A>, E.Obs<A>, step(~A, ~cmp, xs, op))))
70
71# ---- the sorted-multiset model: order and removal ----
72
73def all_ge(~A: Data, ~cmp: A -> A -> Cmp, +z: A, xs: List<&2, A>) -> Bool:
74 match xs:
75 case Nil{}:
76 True{}
77 case Con{h, t}:
78 Bool.and(le(~A, ~cmp, z, h), all_ge(~A, ~cmp, z, t))
79
80def sorted(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> Bool:
81 match xs:
82 case Nil{}:
83 True{}
84 case Con{+h, +t}:
85 Bool.and(all_ge(~A, ~cmp, h, t), sorted(~A, ~cmp, t))
86
87def eq_head(~A: Data, ~cmp: A -> A -> Cmp, +z: A, xs: List<&2, A>) -> Bool:
88 match xs:
89 case Nil{}:
90 False{}
91 case Con{h, t}:
92 Cmp.is_eq(cmp(z, h))
93
94def del(~A: Data, ~cmp: A -> A -> Cmp, +z: A, xs: List<&2, A>, b: Bool) -> List<&2, A>:
95 match xs b:
96 case Nil{} _:
97 Nil{}
98 case Con{h, t} True{}:
99 t
100 case Con{h, +t} False{}:
101 Con{h, del(~A, ~cmp, z, t, eq_head(~A, ~cmp, z, t))}
102
103def delf(~A: Data, ~cmp: A -> A -> Cmp, +z: A, +xs: List<&2, A>) -> List<&2, A>:
104 del(~A, ~cmp, z, xs, eq_head(~A, ~cmp, z, xs))
105
106# ---- contract (SPARK formal containers) ----
107# Each `<Subprogram>.<clause>` definition below states one Post clause of
108# that SPARK subprogram, as a proposition on this model; the table names the
109# clauses. proofs/containers/binary_heap/ proves every clause under its clause name,
110# and its `impl` lemma carries them to the implementation.
111#
112# Contracts of the binary heap. SPARKlib has no formal priority queue, so
113# these are the SPARK-style contracts of the closest container: a sorted
114# multiset, the model S uses (the ascending list of the elements, which is
115# unique for each multiset; SPARKlib src/full/spark-containers-formal-
116# ordered_sets.ads, AdaCore/SPARKlib 46ec319, with multiplicity). Each lemma
117# is one Post clause of step, under a total order ~o; `impl` (via
118# P.step_ok) carries every clause to the implementation.
119#
120# contract (closest SPARK subprogram) ours lemmas
121# Length (ordered_sets 112) length length_result, length_frame
122# Empty_Set (99) new new_empty
123# Insert, with multiplicity (777) push push_length, push_bag, push_sorted
124# First_Element: the minimum (1534) peek peek_min, peek_frame, peek_empty
125# Delete_First (1105) pop pop_length, pop_result, pop_min,
126# pop_bag, pop_empty
127# To_Set (559) from_list from_list_model, from_list_length,
128# from_list_sorted
129# Elements / iteration (ordered) to_sorted_list to_sorted_result, to_sorted_frame
130# every model is ordered model_sorted
131# implementation H.step impl
132# Pop's result is the minimum and its model is the rest: Delete_First on a
133# multiset (First_Element'Old removed once, pop_bag), and push adds exactly
134# one occurrence (push_bag: removing it gives the old multiset back). Not
135# applicable: a heap has no keys, cursors or positions (Find, Floor,
136# Ceiling, Next, Previous, Contains, Replace, Exclude of an arbitrary
137# element, Last_Element), and no set algebra.
138
139def nx(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +op: E.Op<A>) -> List<&2, A>:
140 Pair.fst(List<&2, A>, E.Obs<A>, step(~A, ~cmp, xs, op))
141
142def ob(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +op: E.Op<A>) -> E.Obs<A>:
143 Pair.snd(List<&2, A>, E.Obs<A>, step(~A, ~cmp, xs, op))
144
145# Length (ordered_sets 112)
146def Length.length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
147 {ob(~A, ~cmp, xs, E.Length{}) == E.ONat{C.length(A, xs)} : E.Obs<A>}
148
149# Length (ordered_sets 112)
150def Length.length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
151 {nx(~A, ~cmp, xs, E.Length{}) == xs : List<&2, A>}
152
153# Insert, with multiplicity (777)
154def Insert.push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> Type:
155 {C.length(A, nx(~A, ~cmp, xs, E.Push{x})) == 1n+C.length(A, xs) : Nat}
156
157# Insert, with multiplicity (777)
158def Insert.push_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A) -> Type:
159 {delf(~A, ~cmp, x, nx(~A, ~cmp, xs, E.Push{x})) == xs : List<&2, A>}
160
161# Insert, with multiplicity (777)
162def Insert.push_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A, +hs: {sorted(~A, ~cmp, xs) == True{} : Bool}) -> Type:
163 {sorted(~A, ~cmp, nx(~A, ~cmp, xs, E.Push{x})) == True{} : Bool}
164
165# First_Element: the minimum (1534)
166def First_Element.peek_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
167 {ob(~A, ~cmp, Con{h, t}, E.Peek{}) == E.OItem{Done{h}} : E.Obs<A>} & {all_ge(~A, ~cmp, h, t) == True{} : Bool}
168
169# First_Element: the minimum (1534)
170def First_Element.peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
171 {nx(~A, ~cmp, xs, E.Peek{}) == xs : List<&2, A>}
172
173# First_Element: the minimum (1534)
174def First_Element.peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
175 {step(~A, ~cmp, Nil{}, E.Peek{}) == (Nil{}, E.OItem{Fail{E.EmptyHeap{}}}) : List<&2, A> & E.Obs<A>}
176
177# Delete_First (1105)
178def Delete_First.pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:
179 {1n+C.length(A, nx(~A, ~cmp, Con{h, t}, E.Pop{})) == C.length(A, Con{h, t}) : Nat}
180
181# Delete_First (1105)
182def Delete_First.pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:
183 {ob(~A, ~cmp, Con{h, t}, E.Pop{}) == E.OItem{Done{h}} : E.Obs<A>}
184
185# Delete_First (1105)
186def Delete_First.pop_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
187 {all_ge(~A, ~cmp, h, nx(~A, ~cmp, Con{h, t}, E.Pop{})) == True{} : Bool}
188
189# Delete_First (1105)
190def Delete_First.pop_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +h: A, +t: List<&2, A>, +hs: {sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
191 {ins(~A, ~cmp, h, nx(~A, ~cmp, Con{h, t}, E.Pop{})) == Con{h, t} : List<&2, A>}
192
193# Delete_First (1105)
194def Delete_First.pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
195 {step(~A, ~cmp, Nil{}, E.Pop{}) == (Nil{}, E.OItem{Fail{E.EmptyHeap{}}}) : List<&2, A> & E.Obs<A>}
196
197# To_Set (559)
198def To_Set.from_list_model(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
199 {nx(~A, ~cmp, xs, E.FromList{ys}) == from_list(~A, ~cmp, ys, Nil{}) : List<&2, A>}
200
201# To_Set (559)
202def To_Set.from_list_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
203 {C.length(A, nx(~A, ~cmp, xs, E.FromList{ys})) == C.length(A, ys) : Nat}
204
205# To_Set (559)
206def To_Set.from_list_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
207 {sorted(~A, ~cmp, nx(~A, ~cmp, xs, E.FromList{ys})) == True{} : Bool}
208
209# Elements / iteration (ordered)
210def Elements.to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
211 {ob(~A, ~cmp, xs, E.ToSortedList{}) == E.OList{xs} : E.Obs<A>}
212
213# Elements / iteration (ordered)
214def Elements.to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
215 {nx(~A, ~cmp, xs, E.ToSortedList{}) == xs : List<&2, A>}