spec/containers/queue.bend
bend-collections-laws-containers@1.0.0.0 · 138 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/queue.bend as E
4import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
5
6# Independent model: a FIFO queue is the sequence of its elements, oldest
7# first. Enqueue appends at the end; dequeue removes the first element.
8
9def item(-T: Data, x: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
10 match x:
11 case None{}:
12 Fail{E.EmptyQueue{}}
13 case Some{v}:
14 Done{v}
15
16def dequeue(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>:
17 match xs:
18 case Nil{}:
19 (Nil{}, E.OItem{Fail{E.EmptyQueue{}}})
20 case Con{h, t}:
21 (t, E.OItem{Done{h}})
22
23def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>:
24 match op:
25 case E.Length{}:
26 (xs, E.ONat{C.length(T, xs)})
27 case E.Enqueue{x}:
28 (C.snoc(T, xs, x), E.OUnit{})
29 case E.Dequeue{}:
30 dequeue(T, xs)
31 case E.Peek{}:
32 (xs, E.OItem{item(T, C.head(T, xs))})
33 case E.ToList{}:
34 (xs, E.OList{xs})
35
36def 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>>:
37 (m, os) = r
38 (m, Con{o, os})
39
40def run(-T: Data, ops: List<&2, E.Op<T>>, +xs: List<&2, T>) -> List<&2, T> & List<&2, E.Obs<T>>:
41 match ops:
42 case Nil{}:
43 (xs, Nil{})
44 case Con{+op, rest}:
45 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))))
46
47# ---- contract (SPARK formal containers) ----
48# Each `<Subprogram>.<clause>` definition below states one Post clause of
49# that SPARK subprogram, as a proposition on this model; the table names the
50# clauses. proofs/containers/queue/ proves every clause under its clause name,
51# and its `impl` lemma carries them to the implementation.
52#
53# Contracts of the FIFO queue in the style of SPARK's formal vectors
54# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
55# 46ec319; model predicates in spec/lib/sequence.bend). The model is the
56# sequence oldest first: enqueue is Append, dequeue is Delete_First, peek
57# is First_Element. Each lemma is one Post clause of step; `impl` (via
58# PS.step_ok) carries every clause to the implementation: Q.step on the
59# queue of a shadow lands on the queue of a shadow whose model satisfies it.
60#
61# SPARK subprogram (.ads line) ours clauses
62# Length (284) length length_result, length_frame
63# Empty_Vector (292) new new_empty, new_impl
64# Append (706) enqueue enqueue_length, enqueue_prefix, enqueue_element
65# Delete_First (825) dequeue dequeue_length, dequeue_shifted,
66# dequeue_result, dequeue_empty
67# First_Element (913) peek peek_first, peek_frame, peek_empty
68# iteration (Iter_Model, 1193) to_list to_list_model, to_list_frame
69# implementation Q.step impl
70# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,
71# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,
72# Reference, Insert*, Prepend*, Append_Vector/Count, Delete (at an index),
73# Delete_Last, Last_Element, Reverse_Elements, Swap, Find_Index,
74# Reverse_Find_Index, Contains, Has_Element. SPARK's Pre (not Is_Empty) is
75# a defensive check: on an empty queue dequeue and peek return EmptyQueue
76# and change nothing.
77
78def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>:
79 Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))
80
81def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>:
82 Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))
83
84# Length (284)
85def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
86 {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
87
88# Length (284)
89def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
90 {nx(T, xs, E.Length{}) == xs : List<&2, T>}
91
92# iteration (Iter_Model, 1193)
93def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
94 {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}
95
96# iteration (Iter_Model, 1193)
97def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
98 {nx(T, xs, E.ToList{}) == xs : List<&2, T>}
99
100# Append (706)
101def Append.enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
102 {C.length(T, nx(T, xs, E.Enqueue{v})) == 1n+C.length(T, xs) : Nat}
103
104# Append (706)
105def Append.enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
106 V.EqualPrefix(T, xs, nx(T, xs, E.Enqueue{v}))
107
108# Append (706)
109def Append.enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
110 {C.nth(T, nx(T, xs, E.Enqueue{v}), C.length(T, xs)) == Some{v} : Maybe<&2, T>}
111
112# Delete_First (825)
113def Delete_First.dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
114 {1n+C.length(T, nx(T, Con{h, t}, E.Dequeue{})) == C.length(T, Con{h, t}) : Nat}
115
116# Delete_First (825)
117def Delete_First.dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
118 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)
119
120# Delete_First (825)
121def Delete_First.dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
122 {ob(T, Con{h, t}, E.Dequeue{}) == E.OItem{Done{h}} : E.Obs<T>}
123
124# Delete_First (825)
125def Delete_First.dequeue_empty(-T: Data) -> Type:
126 {step(T, Nil{}, E.Dequeue{}) == (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) : List<&2, T> & E.Obs<T>}
127
128# First_Element (913)
129def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
130 {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>}
131
132# First_Element (913)
133def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type:
134 {nx(T, xs, E.Peek{}) == xs : List<&2, T>}
135
136# First_Element (913)
137def First_Element.peek_empty(-T: Data) -> Type:
138 {step(T, Nil{}, E.Peek{}) == (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) : List<&2, T> & E.Obs<T>}