|
(* Author: Tobias Nipkow *)
section \<open>Queue Specification\<close>
theory Queue_Spec
imports Main
begin
text \<open>The basic queue interface with \<open>list\<close>-based specification:\<close>
locale Queue =
fixes empty :: "'q"
fixes enq :: "'a \ 'q \ 'q"
fixes first :: "'q \ 'a"
fixes deq :: "'q \ 'q"
fixes is_empty :: "'q \ bool"
fixes list :: "'q \ 'a list"
fixes invar :: "'q \ bool"
assumes list_empty: "list empty = []"
assumes list_enq: "invar q \ list(enq x q) = list q @ [x]"
assumes list_deq: "invar q \ list(deq q) = tl(list q)"
assumes list_first: "invar q \ \ list q = [] \ first q = hd(list q)"
assumes list_is_empty: "invar q \ is_empty q = (list q = [])"
assumes invar_empty: "invar empty"
assumes invar_enq: "invar q \ invar(enq x q)"
assumes invar_deq: "invar q \ invar(deq q)"
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
