Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Array_Specs.thy Sprache: Isabelle

Original von: Isabelle^©

theory Array_Specs
imports Main
begin

text \<open>Array Specifications\<close>

locale Array =
fixes lookup :: "'ar \ nat \ 'a"
fixes update :: "nat \ 'a \ 'ar \ 'ar"
fixes len :: "'ar \ nat"
fixes array :: "'a list \ 'ar"

fixes list :: "'ar \ 'a list"
fixes invar :: "'ar \ bool"

assumes lookup: "invar ar \ n < len ar \ lookup ar n = list ar ! n"
assumes update: "invar ar \ n < len ar \ list(update n x ar) = (list ar)[n:=x]"
assumes len_array: "invar ar \ len ar = length (list ar)"
assumes array: "list (array xs) = xs"

assumes invar_update: "invar ar \ n < len ar \ invar(update n x ar)"
assumes invar_array: "invar(array xs)"

locale Array_Flex = Array +
fixes add_lo :: "'a \ 'ar \ 'ar"
fixes del_lo :: "'ar \ 'ar"
fixes add_hi :: "'a \ 'ar \ 'ar"
fixes del_hi :: "'ar \ 'ar"

assumes add_lo: "invar ar \ list(add_lo a ar) = a # list ar"
assumes del_lo: "invar ar \ list(del_lo ar) = tl (list ar)"
assumes add_hi: "invar ar \ list(add_hi a ar) = list ar @ [a]"
assumes del_hi: "invar ar \ list(del_hi ar) = butlast (list ar)"

assumes invar_add_lo: "invar ar \ invar (add_lo a ar)"
assumes invar_del_lo: "invar ar \ invar (del_lo ar)"
assumes invar_add_hi: "invar ar \ invar (add_hi a ar)"
assumes invar_del_hi: "invar ar \ invar (del_hi ar)"

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.