Quelle Queue_Spec.thy Sprache: 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

quality34%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.