Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Wellfounded_More.thy Sprache: Isabelle

Original von: Isabelle^©

(* 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) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.