spec/containers/deque.bend source
spec/containers/deque.bend on the hub · documented module
import Baseimport ../lib/common.bend as Cimport ../../src/containers/types/deque.bend as Eimport ../lib/sequence.bend as V# Independent model: a deque is the finite sequence of its elements, front# first. Nothing here refers to the two-list representation.def item(-T: Data, x: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>: match x: case None{}: Fail{E.EmptyDeque{}} case Some{v}: Done{v}def pop_front(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>: match xs: case Nil{}: (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) case Con{h, t}: (t, E.OItem{Done{h}})def pop_back(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>: match xs: case Nil{}: (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) case Con{+h, +t}: (C.init(T, Con{h, t}), E.OItem{item(T, C.last(T, Con{h, t}))})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.PushFront{x}: (Con{x, xs}, E.OUnit{}) case E.PushBack{x}: (C.snoc(T, xs, x), E.OUnit{}) case E.PopFront{}: pop_front(T, xs) case E.PopBack{}: pop_back(T, xs) case E.PeekFront{}: (xs, E.OItem{item(T, C.head(T, xs))}) case E.PeekBack{}: (xs, E.OItem{item(T, C.last(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/deque/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the deque 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 front first. Each lemma is one Post clause of step; `impl`# (via P.step_ok) carries every clause to the implementation: DQ.step on# the deque of a shadow lands on the deque 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# Prepend (624) push_front push_front_length, push_front_first, push_front_shifted# Append (706) push_back push_back_length, push_back_prefix, push_back_element# Delete_First (825) pop_front pop_front_length, pop_front_shifted,# pop_front_result, pop_front_empty# Delete_Last (866) pop_back pop_back_length, pop_back_prefix,# pop_back_result, pop_back_empty# First_Element (913) peek_front peek_front_first, peek_front_frame, peek_front_empty# Last_Element (923) peek_back peek_back_last, peek_back_frame, peek_back_empty# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame# implementation DQ.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 with Count or a vector, Delete (at an# index or a count), Reverse_Elements, Swap, Find_Index, Reverse_Find_Index,# Contains, Has_Element. SPARK's Pre (not Is_Empty) is a defensive check:# on an empty deque pops and peeks return EmptyDeque 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>}# Prepend (624)def Prepend.push_front_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.length(T, nx(T, xs, E.PushFront{v})) == 1n+C.length(T, xs) : Nat}# Prepend (624)def Prepend.push_front_first(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.nth(T, nx(T, xs, E.PushFront{v}), 0n) == Some{v} : Maybe<&2, T>}# Prepend (624)def Prepend.push_front_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> Type: V.RangeShifted(T, xs, nx(T, xs, E.PushFront{v}), 0n, C.length(T, xs), 1n)# Append (706)def Append.push_back_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.length(T, nx(T, xs, E.PushBack{v})) == 1n+C.length(T, xs) : Nat}# Append (706)def Append.push_back_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type: V.EqualPrefix(T, xs, nx(T, xs, E.PushBack{v}))# Append (706)def Append.push_back_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.nth(T, nx(T, xs, E.PushBack{v}), C.length(T, xs)) == Some{v} : Maybe<&2, T>}# Delete_First (825)def Delete_First.pop_front_length(-T: Data, +h: T, +t: List<&2, T>) -> Type: {1n+C.length(T, nx(T, Con{h, t}, E.PopFront{})) == C.length(T, Con{h, t}) : Nat}# Delete_First (825)def Delete_First.pop_front_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type: V.RangeShifted(T, nx(T, Con{h, t}, E.PopFront{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.PopFront{})), 1n)# Delete_First (825)def Delete_First.pop_front_result(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.PopFront{}) == E.OItem{Done{h}} : E.Obs<T>}# Delete_First (825)def Delete_First.pop_front_empty(-T: Data) -> Type: {step(T, Nil{}, E.PopFront{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}# Delete_Last (866)def Delete_Last.pop_back_length(-T: Data, +h: T, +t: List<&2, T>) -> Type: {C.length(T, nx(T, Con{h, t}, E.PopBack{})) == C.length(T, t) : Nat}# Delete_Last (866)def Delete_Last.pop_back_prefix(-T: Data, +h: T, +t: List<&2, T>) -> Type: V.EqualPrefix(T, nx(T, Con{h, t}, E.PopBack{}), Con{h, t})# Delete_Last (866)def Delete_Last.pop_back_result(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.PopBack{}) == E.OItem{item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}# Delete_Last (866)def Delete_Last.pop_back_empty(-T: Data) -> Type: {step(T, Nil{}, E.PopBack{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}# First_Element (913)def First_Element.peek_front_first(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.PeekFront{}) == 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_front_frame(-T: Data, +xs: List<&2, T>) -> Type: {nx(T, xs, E.PeekFront{}) == xs : List<&2, T>}# First_Element (913)def First_Element.peek_front_empty(-T: Data) -> Type: {step(T, Nil{}, E.PeekFront{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}# Last_Element (923)def Last_Element.peek_back_last(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.PeekBack{}) == E.OItem{item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}# Last_Element (923)def Last_Element.peek_back_frame(-T: Data, +xs: List<&2, T>) -> Type: {nx(T, xs, E.PeekBack{}) == xs : List<&2, T>}# Last_Element (923)def Last_Element.peek_back_empty(-T: Data) -> Type: {step(T, Nil{}, E.PeekBack{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}