proofs/containers/simple_queue/proof.bend
bend-collections-laws-containers@1.0.0.0 · 82 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/simple_queue.bend as P1
3import bend-collections-laws-containers@1.0.0.0/src/containers/queue.bend as K1
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/queue.bend as E1
5import bend-collections-laws-containers@1.0.0.0/spec/containers/simple_queue.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/proof.bend as UP
7
8# src/containers/simple_queue.bend: a FIFO queue behind the queue interface (put = enqueue, get = dequeue, qsize = length).
9
10def simple_queue_put(q: K1.Queue<U32>, +v: U32) -> {P1.put(~U32, q, v) == K1.enqueue(~U32, q, v) : K1.Queue<U32>}:
11 {==}
12
13def simple_queue_get(q: K1.Queue<U32>) -> {P1.get(~U32, q) == K1.dequeue(~U32, q) : K1.Queue<U32> & Result<&2, &2, E1.Error, U32>}:
14 {==}
15
16def simple_queue_qsize(q: K1.Queue<U32>) -> {P1.qsize(~U32, q) == K1.length(~U32, q) : K1.Queue<U32> & Nat}:
17 {==}
18
19# ==== the contract of simple_queue (stated in spec/containers/simple_queue.bend) ====================
20
21def new_is(~T: Data) -> {P1.new(~T) == K1.new(~T) : K1.Queue<T>}:
22 {==}
23
24def qsize_is(~T: Data, q: K1.Queue<T>) -> {P1.qsize(~T, q) == K1.length(~T, q) : K1.Queue<T> & Nat}:
25 {==}
26
27def put_is(~T: Data, q: K1.Queue<T>, x: T) -> {P1.put(~T, q, x) == K1.enqueue(~T, q, x) : K1.Queue<T>}:
28 {==}
29
30def get_is(~T: Data, q: K1.Queue<T>) -> {P1.get(~T, q) == K1.dequeue(~T, q) : K1.Queue<T> & Result<&2, &2, E1.Error, T>}:
31 {==}
32
33def peek_is(~T: Data, q: K1.Queue<T>) -> {P1.peek(~T, q) == K1.peek(~T, q) : K1.Queue<T> & Result<&2, &2, E1.Error, T>}:
34 {==}
35
36def to_list_is(~T: Data, q: K1.Queue<T>) -> {P1.to_list(~T, q) == K1.to_list(~T, q) : K1.Queue<T> & List<&2, T>}:
37 {==}
38
39# ---- the queue's contract, carried: every clause is proved by the queue ----
40
41def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):
42 UP.length_result(T, xs)
43
44def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):
45 UP.length_frame(T, xs)
46
47def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):
48 UP.to_list_model(T, xs)
49
50def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):
51 UP.to_list_frame(T, xs)
52
53def enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_length(T, xs, v):
54 UP.enqueue_length(T, xs, v)
55
56def enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_prefix(T, xs, v):
57 UP.enqueue_prefix(T, xs, v)
58
59def enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_element(T, xs, v):
60 UP.enqueue_element(T, xs, v)
61
62def dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_length(T, h, t):
63 UP.dequeue_length(T, h, t)
64
65def dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_shifted(T, h, t):
66 UP.dequeue_shifted(T, h, t)
67
68def dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_result(T, h, t):
69 UP.dequeue_result(T, h, t)
70
71def dequeue_empty(-T: Data) -> S.Delete_First.dequeue_empty(T):
72 UP.dequeue_empty(T)
73
74def peek_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_first(T, h, t):
75 UP.peek_first(T, h, t)
76
77def peek_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_frame(T, xs):
78 UP.peek_frame(T, xs)
79
80def peek_empty(-T: Data) -> S.First_Element.peek_empty(T):
81 UP.peek_empty(T)
82