Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMSL/DFDexampleSL/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 13.4.2020 mit Größe 65 kB

Impressum 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.1 Sekunden (vorverarbeitet) ¤

*Bot Zugriff

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.