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