|
72389
|
1 |
(* Author: Tobias Nipkow *)
|
|
|
2 |
|
|
|
3 |
section \<open>Queue Specification\<close>
|
|
|
4 |
|
|
|
5 |
theory Queue_Spec
|
|
|
6 |
imports Main
|
|
|
7 |
begin
|
|
|
8 |
|
|
|
9 |
text \<open>The basic queue interface with \<open>list\<close>-based specification:\<close>
|
|
|
10 |
|
|
|
11 |
locale Queue =
|
|
|
12 |
fixes empty :: "'q"
|
|
|
13 |
fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q"
|
|
72485
|
14 |
fixes first :: "'q \<Rightarrow> 'a"
|
|
72389
|
15 |
fixes deq :: "'q \<Rightarrow> 'q"
|
|
|
16 |
fixes is_empty :: "'q \<Rightarrow> bool"
|
|
|
17 |
fixes list :: "'q \<Rightarrow> 'a list"
|
|
|
18 |
fixes invar :: "'q \<Rightarrow> bool"
|
|
|
19 |
assumes list_empty: "list empty = []"
|
|
|
20 |
assumes list_enq: "invar q \<Longrightarrow> list(enq x q) = list q @ [x]"
|
|
|
21 |
assumes list_deq: "invar q \<Longrightarrow> list(deq q) = tl(list q)"
|
|
72485
|
22 |
assumes list_first: "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> first q = hd(list q)"
|
|
72389
|
23 |
assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])"
|
|
|
24 |
assumes invar_empty: "invar empty"
|
|
|
25 |
assumes invar_enq: "invar q \<Longrightarrow> invar(enq x q)"
|
|
|
26 |
assumes invar_deq: "invar q \<Longrightarrow> invar(deq q)"
|
|
|
27 |
|
|
|
28 |
end
|