spec/containers/stack.bend source
spec/containers/stack.bend on the hub · documented module
import Baseimport ../lib/common.bend as Cimport ../../src/containers/types/stack.bend as Eimport ../lib/sequence.bend as V# Independent LIFO sequence model; top is the first element.def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>: match xs op: case +ys E.Push{x}: (Con{x, ys}, E.OUnit{}) case +ys E.Length{}: (ys, E.ONat{C.length(T, ys)}) case +ys E.ToList{}: (ys, E.OList{ys}) case Nil{} E.Pop{}: (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) case Con{x, tail} E.Pop{}: (tail, E.OItem{Done{x}}) case Nil{} E.Peek{}: (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) case Con{+x, +tail} E.Peek{}: (Con{x, tail}, E.OItem{Done{x}})# ---- 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/stack/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the stack 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 with the top first, so push is Prepend, pop is Delete_First and# peek is First_Element. Each lemma is one Post clause of step; `impl`# (P.step_correct: D.step on the stack of a sequence is step lifted)# carries every clause to the implementation.## SPARK subprogram (.ads line) ours clauses# Length (284) length length_result, length_frame# Empty_Vector (292) new new_empty, new_impl# Prepend (624) push push_length, push_first, push_shifted# Delete_First (825) pop pop_length, pop_shifted, pop_result, pop_empty# First_Element (913) peek peek_first, peek_frame, peek_empty# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame# implementation D.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*, Append*, 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 stack pop and peek return EmptyStack and change nothing# (pop_empty, peek_empty).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>}# Empty_Vector (292)def Empty_Vector.new_empty(-T: Data) -> Type: {C.length(T, Nil{}) == 0n : Nat}# Prepend (624)def Prepend.push_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.length(T, nx(T, xs, E.Push{v})) == 1n+C.length(T, xs) : Nat}# Prepend (624)def Prepend.push_first(-T: Data, +xs: List<&2, T>, +v: T) -> Type: {C.nth(T, nx(T, xs, E.Push{v}), 0n) == Some{v} : Maybe<&2, T>}# Prepend (624)def Prepend.push_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> Type: V.RangeShifted(T, xs, nx(T, xs, E.Push{v}), 0n, C.length(T, xs), 1n)# Delete_First (825)def Delete_First.pop_length(-T: Data, +h: T, +t: List<&2, T>) -> Type: {1n+C.length(T, nx(T, Con{h, t}, E.Pop{})) == C.length(T, Con{h, t}) : Nat}# Delete_First (825)def Delete_First.pop_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type: V.RangeShifted(T, nx(T, Con{h, t}, E.Pop{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.Pop{})), 1n)# Delete_First (825)def Delete_First.pop_result(-T: Data, +h: T, +t: List<&2, T>) -> Type: {ob(T, Con{h, t}, E.Pop{}) == E.OItem{Done{h}} : E.Obs<T>}# Delete_First (825)def Delete_First.pop_empty(-T: Data) -> Type: {step(T, Nil{}, E.Pop{}) == (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) : 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.EmptyStack{}}}) : List<&2, T> & E.Obs<T>}