spec/containers/priority_queue.bend source

spec/containers/priority_queue.bend on the hub · documented module

import Baseimport ../lib/order.bend as SOimport ./binary_heap.bend as HS# ---- contract (SPARK formal containers) ----# Each `<Subprogram>.<clause>` definition below states one Post clause of# that SPARK subprogram, as a proposition on this model; the table names the# clauses. proofs/containers/priority_queue/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## The priority queue is the binary heap behind another interface; every one# of its operations is the heap's (for every element type and order), so it# has the heap's SPARK-style multiset contracts,# spec/containers/binary_heap.bend (restated below):##   contract                 priority_queue   binary_heap      contract lemmas (HC.)#   Empty_Set                new              new              new_empty#   Length                   qsize            length           length_result, length_frame#   Insert (multiplicity)    put              push             push_length, push_bag, push_sorted#   First_Element (minimum)  peek             peek             peek_min, peek_frame, peek_empty#   Delete_First (minimum)   get              pop              pop_length, pop_result, pop_min,#                                                              pop_bag, pop_empty#   To_Set                   from_list        from_list        from_list_model, from_list_length,#                                                              from_list_sorted#   Elements (ordered)       to_sorted_list   to_sorted_list   to_sorted_result, to_sorted_frame#   implementation                                             HC.impl, HC.model_sorted# The model is the binary_heap's (HS.step) and so is every clause:def Length.length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:  HS.Length.length_result(~A, ~cmp, xs)def Length.length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:  HS.Length.length_frame(~A, ~cmp, xs)def Insert.push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> Type:  HS.Insert.push_length(~A, ~cmp, xs, x)def Insert.push_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A) -> Type:  HS.Insert.push_bag(~A, ~cmp, ~o, xs, x)def 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:  HS.Insert.push_sorted(~A, ~cmp, ~o, xs, x, hs)def 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:  HS.First_Element.peek_min(~A, ~cmp, h, t, hs)def First_Element.peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:  HS.First_Element.peek_frame(~A, ~cmp, xs)def First_Element.peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:  HS.First_Element.peek_empty(~A, ~cmp)def Delete_First.pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:  HS.Delete_First.pop_length(~A, ~cmp, h, t)def Delete_First.pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:  HS.Delete_First.pop_result(~A, ~cmp, h, t)def 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:  HS.Delete_First.pop_min(~A, ~cmp, h, t, hs)def 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:  HS.Delete_First.pop_bag(~A, ~cmp, ~o, h, t, hs)def Delete_First.pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:  HS.Delete_First.pop_empty(~A, ~cmp)def To_Set.from_list_model(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:  HS.To_Set.from_list_model(~A, ~cmp, xs, ys)def To_Set.from_list_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:  HS.To_Set.from_list_length(~A, ~cmp, xs, ys)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:  HS.To_Set.from_list_sorted(~A, ~cmp, ~o, xs, ys)def Elements.to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:  HS.Elements.to_sorted_result(~A, ~cmp, xs)def Elements.to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:  HS.Elements.to_sorted_frame(~A, ~cmp, xs)