9 text \<open>The basic queue interface with \<open>list\<close>-based specification:\<close> |
9 text \<open>The basic queue interface with \<open>list\<close>-based specification:\<close> |
10 |
10 |
11 locale Queue = |
11 locale Queue = |
12 fixes empty :: "'q" |
12 fixes empty :: "'q" |
13 fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q" |
13 fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q" |
14 fixes front :: "'q \<Rightarrow> 'a" |
14 fixes first :: "'q \<Rightarrow> 'a" |
15 fixes deq :: "'q \<Rightarrow> 'q" |
15 fixes deq :: "'q \<Rightarrow> 'q" |
16 fixes is_empty :: "'q \<Rightarrow> bool" |
16 fixes is_empty :: "'q \<Rightarrow> bool" |
17 fixes list :: "'q \<Rightarrow> 'a list" |
17 fixes list :: "'q \<Rightarrow> 'a list" |
18 fixes invar :: "'q \<Rightarrow> bool" |
18 fixes invar :: "'q \<Rightarrow> bool" |
19 assumes list_empty: "list empty = []" |
19 assumes list_empty: "list empty = []" |
20 assumes list_enq: "invar q \<Longrightarrow> list(enq x q) = list q @ [x]" |
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)" |
21 assumes list_deq: "invar q \<Longrightarrow> list(deq q) = tl(list q)" |
22 assumes list_front: "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> front q = hd(list q)" |
22 assumes list_first: "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> first q = hd(list q)" |
23 assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])" |
23 assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])" |
24 assumes invar_empty: "invar empty" |
24 assumes invar_empty: "invar empty" |
25 assumes invar_enq: "invar q \<Longrightarrow> invar(enq x q)" |
25 assumes invar_enq: "invar q \<Longrightarrow> invar(enq x q)" |
26 assumes invar_deq: "invar q \<Longrightarrow> invar(deq q)" |
26 assumes invar_deq: "invar q \<Longrightarrow> invar(deq q)" |
27 |
27 |