blob: 9f7eb5347347f81e69772ecac2034e400535eec5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
// Queue.dfyi
abstract module Queue {
type Item
type Queue = seq<Item>
method Init() returns (q: Queue)
ensures |q| == 0;
method Push(item: Item, q: Queue) returns (q': Queue)
ensures |q'| == |q| + 1;
method Pop(q: Queue) returns (item: Item, q': Queue)
requires |q| > 0;
ensures item in q;
ensures |q'| == |q| - 1;
}
abstract module MainSpec {
import Q as Queue
}
|