Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Isabelle

Original von: Isabelle^©

(* Author: Tobias Nipkow, Peter Lammich *)

section \<open>Priority Queue Specifications\<close>

theory Priority_Queue_Specs
imports "HOL-Library.Multiset"
begin

text \<open>Priority queue interface + specification:\<close>

locale Priority_Queue =
fixes empty :: "'q"
and is_empty :: "'q \ bool"
and insert :: "'a::linorder \ 'q \ 'q"
and get_min :: "'q \ 'a"
and del_min :: "'q \ 'q"
and invar :: "'q \ bool"
and mset :: "'q \ 'a multiset"
assumes mset_empty: "mset empty = {#}"
and is_empty: "invar q \ is_empty q = (mset q = {#})"
and mset_insert: "invar q \ mset (insert x q) = mset q + {#x#}"
and mset_del_min: "invar q \ mset q \ {#} \
mset (del_min q) = mset q - {# get_min q #}"
and mset_get_min: "invar q \ mset q \ {#} \ get_min q = Min_mset (mset q)"
and invar_empty: "invar empty"
and invar_insert: "invar q \ invar (insert x q)"
and invar_del_min: "invar q \ mset q \ {#} \ invar (del_min q)"

text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>

locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
fixes merge :: "'q \ 'q \ 'q"
assumes mset_merge: "\ invar q1; invar q2 \ \ mset (merge q1 q2) = mset q1 + mset q2"
and invar_merge: "\ invar q1; invar q2 \ \ invar (merge q1 q2)"

end

¤ Dauer der Verarbeitung: 0.1 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.