spec/containers/stack.bend
bend-collections-laws-containers@1.0.0.0 · 118 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/stack.bend as E
4import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
5
6# Independent LIFO sequence model; top is the first element.
7def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>:
8 match xs op:
9 case +ys E.Push{x}:
10 (Con{x, ys}, E.OUnit{})
11 case +ys E.Length{}:
12 (ys, E.ONat{C.length(T, ys)})
13 case +ys E.ToList{}:
14 (ys, E.OList{ys})
15 case Nil{} E.Pop{}:
16 (Nil{}, E.OItem{Fail{E.EmptyStack{}}})
17 case Con{x, tail} E.Pop{}:
18 (tail, E.OItem{Done{x}})
19 case Nil{} E.Peek{}:
20 (Nil{}, E.OItem{Fail{E.EmptyStack{}}})
21 case Con{+x, +tail} E.Peek{}:
22 (Con{x, tail}, E.OItem{Done{x}})
23
24# ---- contract (SPARK formal containers) ----
25# Each `<Subprogram>.<clause>` definition below states one Post clause of
26# that SPARK subprogram, as a proposition on this model; the table names the
27# clauses. proofs/containers/stack/ proves every clause under its clause name,
28# and its `impl` lemma carries them to the implementation.
29#
30# Contracts of the stack in the style of SPARK's formal vectors
31# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
32# 46ec319; model predicates in spec/lib/sequence.bend). The model is the
33# sequence with the top first, so push is Prepend, pop is Delete_First and
34# peek is First_Element. Each lemma is one Post clause of step; `impl`
35# (P.step_correct: D.step on the stack of a sequence is step lifted)
36# carries every clause to the implementation.
37#
38# SPARK subprogram (.ads line) ours clauses
39# Length (284) length length_result, length_frame
40# Empty_Vector (292) new new_empty, new_impl
41# Prepend (624) push push_length, push_first, push_shifted
42# Delete_First (825) pop pop_length, pop_shifted, pop_result, pop_empty
43# First_Element (913) peek peek_first, peek_frame, peek_empty
44# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame
45# implementation D.step impl
46# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,
47# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,
48# Reference, Insert*, Append*, Delete (at an index), Delete_Last,
49# Last_Element, Reverse_Elements, Swap, Find_Index, Reverse_Find_Index,
50# Contains, Has_Element. SPARK's Pre (not Is_Empty) is a defensive check:
51# on an empty stack pop and peek return EmptyStack and change nothing
52# (pop_empty, peek_empty).
53
54def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>:
55 Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))
56
57def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>:
58 Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))
59
60# Length (284)
61def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
62 {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
63
64# Length (284)
65def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
66 {nx(T, xs, E.Length{}) == xs : List<&2, T>}
67
68# iteration (Iter_Model, 1193)
69def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
70 {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}
71
72# iteration (Iter_Model, 1193)
73def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
74 {nx(T, xs, E.ToList{}) == xs : List<&2, T>}
75
76# Empty_Vector (292)
77def Empty_Vector.new_empty(-T: Data) -> Type:
78 {C.length(T, Nil{}) == 0n : Nat}
79
80# Prepend (624)
81def Prepend.push_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
82 {C.length(T, nx(T, xs, E.Push{v})) == 1n+C.length(T, xs) : Nat}
83
84# Prepend (624)
85def Prepend.push_first(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
86 {C.nth(T, nx(T, xs, E.Push{v}), 0n) == Some{v} : Maybe<&2, T>}
87
88# Prepend (624)
89def Prepend.push_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
90 V.RangeShifted(T, xs, nx(T, xs, E.Push{v}), 0n, C.length(T, xs), 1n)
91
92# Delete_First (825)
93def Delete_First.pop_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
94 {1n+C.length(T, nx(T, Con{h, t}, E.Pop{})) == C.length(T, Con{h, t}) : Nat}
95
96# Delete_First (825)
97def Delete_First.pop_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
98 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)
99
100# Delete_First (825)
101def Delete_First.pop_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
102 {ob(T, Con{h, t}, E.Pop{}) == E.OItem{Done{h}} : E.Obs<T>}
103
104# Delete_First (825)
105def Delete_First.pop_empty(-T: Data) -> Type:
106 {step(T, Nil{}, E.Pop{}) == (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) : List<&2, T> & E.Obs<T>}
107
108# First_Element (913)
109def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
110 {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>}
111
112# First_Element (913)
113def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type:
114 {nx(T, xs, E.Peek{}) == xs : List<&2, T>}
115
116# First_Element (913)
117def First_Element.peek_empty(-T: Data) -> Type:
118 {step(T, Nil{}, E.Peek{}) == (Nil{}, E.OItem{Fail{E.EmptyStack{}}}) : List<&2, T> & E.Obs<T>}