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

quality97%

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