spec/containers/queue.bend source
spec/containers/queue.bend on the hub · documented module
import Baseimport ../lib/common.bend as Cimport ../../src/containers/types/queue.bend as Eimport ../lib/sequence.bend as V# Independent model: a FIFO queue is the sequence of its elements, oldest# first. Enqueue appends at the end; dequeue removes the first element.def item(-T: Data, x: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>: match x: case None{}: Fail{E.EmptyQueue{}} case Some{v}: Done{v}def dequeue(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>: match xs: case Nil{}: (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) case Con{h, t}: (t, E.OItem{Done{h}})def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>: match op: case E.Length{}: (xs, E.ONat{C.length(T, xs)}) case E.Enqueue{x}: (C.snoc(T, xs, x), E.OUnit{}) case E.Dequeue{}: dequeue(T, xs) case E.Peek{}: (xs, E.OItem{item(T, C.head(T, xs))}) case E.ToList{}: (xs, E.OList{xs})def 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>>: (m, os) = r (m, Con{o, os})def run(-T: Data, ops: List<&2, E.Op<T>>, +xs: List<&2, T>) -> List<&2, T> & List<&2, E.Obs<T>>: match ops: case Nil{}: (xs, Nil{}) case Con{+op, rest}: 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))))# ---- 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/queue/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the FIFO queue in the style of SPARK's formal vectors# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib# 46ec319; model predicates in spec/lib/sequence.bend). The model is the# sequence oldest first: enqueue is Append, dequeue is Delete_First, peek# is First_Element. Each lemma is one Post clause of step; `impl` (via# PS.step_ok) carries every clause to the implementation: Q.step on the# queue of a shadow lands on the queue of a shadow whose model satisfies it.## SPARK subprogram (.ads line) ours clauses# Length (284) length length_result, length_frame# Empty_Vector (292) new new_empty, new_impl# Append (706) enqueue enqueue_length, enqueue_prefix, enqueue_element# Delete_First (825) dequeue dequeue_length, dequeue_shifted,# dequeue_result, dequeue_empty# First_Element (913) peek peek_first, peek_frame, peek_empty# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame# implementation Q.step impl# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,# Reference, Insert*, Prepend*, Append_Vector/Count, Delete (at an index),# Delete_Last, Last_Element, Reverse_Elements, Swap, Find_Index,# Reverse_Find_Index, Contains, Has_Element. SPARK's Pre (not Is_Empty) is# a defensive check: on an empty queue dequeue and peek return EmptyQueue# and change nothing.def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>: Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>: Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))# Length (284)def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type: {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}# Length (284)def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type: {nx(T, xs, E.Length{}) == xs : List<&2, T>}# iteration (Iter_Model, 1193)def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type: {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}# iteration (Iter_Model, 1193)def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type: {nx(T, xs, E.ToList{}) == xs : List<&2, T>}# Append (706)def Append.enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.length(T, nx(T, xs, E.Enqueue{v})) == 1n+C.length(T, xs) : Nat}# Append (706)def Append.enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type: V.EqualPrefix(T, xs, nx(T, xs, E.Enqueue{v}))# Append (706)def Append.enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.nth(T, nx(T, xs, E.Enqueue{v}), C.length(T, xs)) == Some{v} : Maybe<&2, T>}# Delete_First (825)def Delete_First.dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> Type: {1n+C.length(T, nx(T, Con{h, t}, E.Dequeue{})) == C.length(T, Con{h, t}) : Nat}# Delete_First (825)def Delete_First.dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type: V.RangeShifted(T, nx(T, Con{h, t}, E.Dequeue{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.Dequeue{})), 1n)# Delete_First (825)def Delete_First.dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.Dequeue{}) == E.OItem{Done{h}} : E.Obs<T>}# Delete_First (825)def Delete_First.dequeue_empty(-T: Data) -> Type: {step(T, Nil{}, E.Dequeue{}) == (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) : List<&2, T> & E.Obs<T>}# First_Element (913)def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.Peek{}) == E.OItem{Done{h}} : E.Obs<T>} & {C.nth(T, Con{h, t}, 0n) == Some{h} : Maybe<&2, T>}# First_Element (913)def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type: {nx(T, xs, E.Peek{}) == xs : List<&2, T>}# First_Element (913)def First_Element.peek_empty(-T: Data) -> Type: {step(T, Nil{}, E.Peek{}) == (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) : List<&2, T> & E.Obs<T>}