spec/containers/simple_queue.bend
bend-collections-laws-containers@1.0.0.0 · 67 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/queue.bend as QS
3
4# ---- contract (SPARK formal containers) ----
5# Each `<Subprogram>.<clause>` definition below states one Post clause of
6# that SPARK subprogram, as a proposition on this model; the table names the
7# clauses. proofs/containers/simple_queue/ proves every clause under its clause name,
8# and its `impl` lemma carries them to the implementation.
9#
10# The simple queue is the FIFO queue behind another interface; every one of
11# its operations is the queue's (for every element type), so it has the
12# queue's SPARK formal-vector contracts, spec/containers/queue.bend (restated below):
13#
14# SPARK subprogram simple_queue queue contract lemmas (QC.)
15# Empty_Vector new new new_empty, new_impl
16# Length qsize length length_result, length_frame
17# Append put enqueue enqueue_length, enqueue_prefix, enqueue_element
18# Delete_First get dequeue dequeue_length, dequeue_shifted,
19# dequeue_result, dequeue_empty
20# First_Element peek peek peek_first, peek_frame, peek_empty
21# iteration to_list to_list to_list_model, to_list_frame
22# implementation QC.impl
23
24# The model is the queue's (QS.step) and so is every clause:
25
26def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
27 QS.Length.length_result(T, xs)
28
29def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
30 QS.Length.length_frame(T, xs)
31
32def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
33 QS.Iteration.to_list_model(T, xs)
34
35def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
36 QS.Iteration.to_list_frame(T, xs)
37
38def Append.enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
39 QS.Append.enqueue_length(T, xs, v)
40
41def Append.enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
42 QS.Append.enqueue_prefix(T, xs, v)
43
44def Append.enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
45 QS.Append.enqueue_element(T, xs, v)
46
47def Delete_First.dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
48 QS.Delete_First.dequeue_length(T, h, t)
49
50def Delete_First.dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
51 QS.Delete_First.dequeue_shifted(T, h, t)
52
53def Delete_First.dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
54 QS.Delete_First.dequeue_result(T, h, t)
55
56def Delete_First.dequeue_empty(-T: Data) -> Type:
57 QS.Delete_First.dequeue_empty(T)
58
59def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
60 QS.First_Element.peek_first(T, h, t)
61
62def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type:
63 QS.First_Element.peek_frame(T, xs)
64
65def First_Element.peek_empty(-T: Data) -> Type:
66 QS.First_Element.peek_empty(T)
67