spec/containers/priority_queue.bend
bend-collections-laws-containers@1.0.0.0 · 83 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
3import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as HS
4
5# ---- contract (SPARK formal containers) ----
6# Each `<Subprogram>.<clause>` definition below states one Post clause of
7# that SPARK subprogram, as a proposition on this model; the table names the
8# clauses. proofs/containers/priority_queue/ proves every clause under its clause name,
9# and its `impl` lemma carries them to the implementation.
10#
11# The priority queue is the binary heap behind another interface; every one
12# of its operations is the heap's (for every element type and order), so it
13# has the heap's SPARK-style multiset contracts,
14# spec/containers/binary_heap.bend (restated below):
15#
16# contract priority_queue binary_heap contract lemmas (HC.)
17# Empty_Set new new new_empty
18# Length qsize length length_result, length_frame
19# Insert (multiplicity) put push push_length, push_bag, push_sorted
20# First_Element (minimum) peek peek peek_min, peek_frame, peek_empty
21# Delete_First (minimum) get pop pop_length, pop_result, pop_min,
22# pop_bag, pop_empty
23# To_Set from_list from_list from_list_model, from_list_length,
24# from_list_sorted
25# Elements (ordered) to_sorted_list to_sorted_list to_sorted_result, to_sorted_frame
26# implementation HC.impl, HC.model_sorted
27
28# The model is the binary_heap's (HS.step) and so is every clause:
29
30def Length.length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
31 HS.Length.length_result(~A, ~cmp, xs)
32
33def Length.length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
34 HS.Length.length_frame(~A, ~cmp, xs)
35
36def Insert.push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> Type:
37 HS.Insert.push_length(~A, ~cmp, xs, x)
38
39def Insert.push_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A) -> Type:
40 HS.Insert.push_bag(~A, ~cmp, ~o, xs, x)
41
42def Insert.push_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A, +hs: {HS.sorted(~A, ~cmp, xs) == True{} : Bool}) -> Type:
43 HS.Insert.push_sorted(~A, ~cmp, ~o, xs, x, hs)
44
45def First_Element.peek_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
46 HS.First_Element.peek_min(~A, ~cmp, h, t, hs)
47
48def First_Element.peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
49 HS.First_Element.peek_frame(~A, ~cmp, xs)
50
51def First_Element.peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
52 HS.First_Element.peek_empty(~A, ~cmp)
53
54def Delete_First.pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:
55 HS.Delete_First.pop_length(~A, ~cmp, h, t)
56
57def Delete_First.pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:
58 HS.Delete_First.pop_result(~A, ~cmp, h, t)
59
60def Delete_First.pop_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
61 HS.Delete_First.pop_min(~A, ~cmp, h, t, hs)
62
63def Delete_First.pop_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
64 HS.Delete_First.pop_bag(~A, ~cmp, ~o, h, t, hs)
65
66def Delete_First.pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
67 HS.Delete_First.pop_empty(~A, ~cmp)
68
69def To_Set.from_list_model(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
70 HS.To_Set.from_list_model(~A, ~cmp, xs, ys)
71
72def To_Set.from_list_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
73 HS.To_Set.from_list_length(~A, ~cmp, xs, ys)
74
75def 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:
76 HS.To_Set.from_list_sorted(~A, ~cmp, ~o, xs, ys)
77
78def Elements.to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
79 HS.Elements.to_sorted_result(~A, ~cmp, xs)
80
81def Elements.to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
82 HS.Elements.to_sorted_frame(~A, ~cmp, xs)
83