1	import Base
2	import ./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	
26	def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
27	  QS.Length.length_result(T, xs)
28	
29	def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
30	  QS.Length.length_frame(T, xs)
31	
32	def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
33	  QS.Iteration.to_list_model(T, xs)
34	
35	def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
36	  QS.Iteration.to_list_frame(T, xs)
37	
38	def Append.enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
39	  QS.Append.enqueue_length(T, xs, v)
40	
41	def Append.enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
42	  QS.Append.enqueue_prefix(T, xs, v)
43	
44	def Append.enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
45	  QS.Append.enqueue_element(T, xs, v)
46	
47	def Delete_First.dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
48	  QS.Delete_First.dequeue_length(T, h, t)
49	
50	def Delete_First.dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
51	  QS.Delete_First.dequeue_shifted(T, h, t)
52	
53	def Delete_First.dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
54	  QS.Delete_First.dequeue_result(T, h, t)
55	
56	def Delete_First.dequeue_empty(-T: Data) -> Type:
57	  QS.Delete_First.dequeue_empty(T)
58	
59	def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
60	  QS.First_Element.peek_first(T, h, t)
61	
62	def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type:
63	  QS.First_Element.peek_frame(T, xs)
64	
65	def First_Element.peek_empty(-T: Data) -> Type:
66	  QS.First_Element.peek_empty(T)
67