1 import Base
2 import ../lib/common.bend as C
3 import ../../src/containers/types/binary_heap.bend as E
4 import ../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
12 def 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.
16 def 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.
24 def 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
31 def 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
38 def pop(-A: Data, xs: List<&2, A>) -> List<&2, A> & E.Obs:
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
45 def step(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, op: E.Op) -> List<&2, A> & E.Obs:
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
60 def cons_obs(-A: Data, o: E.Obs, r: List<&2, A> & List<&2, E.Obs>) -> List<&2, A> & List<&2, E.Obs>:
61 (m, os) = r
62 (m, Con{o, os})
63
64 def run(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, +xs: List<&2, A>) -> List<&2, A> & List<&2, E.Obs>:
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, step(~A, ~cmp, xs, op)), run(~A, ~cmp, rest, Pair.fst(List<&2, A>, E.Obs, step(~A, ~cmp, xs, op))))
70
71 # ---- the sorted-multiset model: order and removal ----
72
73 def 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
80 def 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
87 def 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
94 def 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
103 def 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 `.` 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
139 def nx(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +op: E.Op) -> List<&2, A>:
140 Pair.fst(List<&2, A>, E.Obs, step(~A, ~cmp, xs, op))
141
142 def ob(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +op: E.Op) -> E.Obs:
143 Pair.snd(List<&2, A>, E.Obs, step(~A, ~cmp, xs, op))
144
145 # Length (ordered_sets 112)
146 def 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}
148
149 # Length (ordered_sets 112)
150 def 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)
154 def 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)
158 def 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)
162 def 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)
166 def 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} & {all_ge(~A, ~cmp, h, t) == True{} : Bool}
168
169 # First_Element: the minimum (1534)
170 def 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)
174 def 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}
176
177 # Delete_First (1105)
178 def 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)
182 def 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}
184
185 # Delete_First (1105)
186 def 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)
190 def 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)
194 def 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}
196
197 # To_Set (559)
198 def 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)
202 def 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)
206 def 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)
210 def 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}
212
213 # Elements / iteration (ordered)
214 def 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>}