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