Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 7 kB

SSL Map_Specs.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section \<open>Specifications of Map ADT\<close>

theory Map_Specs
imports AList_Upd_Del
begin

text \<open>The basic map interface with @{typ "'a \<Rightarrow> 'b option"} based specification:\<close>

locale Map =
fixes empty :: "'m"
fixes update :: "'a \ 'b \ 'm \ 'm"
fixes delete :: "'a \ 'm \ 'm"
fixes lookup :: "'m \ 'a \ 'b option"
fixes invar :: "'m \ bool"
assumes map_empty: "lookup empty = (\_. None)"
and map_update: "invar m \ lookup(update a b m) = (lookup m)(a := Some b)"
and map_delete: "invar m \ lookup(delete a m) = (lookup m)(a := None)"
and invar_empty: "invar empty"
and invar_update: "invar m \ invar(update a b m)"
and invar_delete: "invar m \ invar(delete a m)"

lemmas (in Map) map_specs =
  map_empty map_update map_delete invar_empty invar_update invar_delete

text \<open>The basic map interface with \<open>inorder\<close>-based specification:\<close>

locale Map_by_Ordered =
fixes empty :: "'t"
fixes update :: "'a::linorder \ 'b \ 't \ 't"
fixes delete :: "'a \ 't \ 't"
fixes lookup :: "'t \ 'a \ 'b option"
fixes inorder :: "'t \ ('a * 'b) list"
fixes inv :: "'t \ bool"
assumes inorder_empty: "inorder empty = []"
and inorder_lookup: "inv t \ sorted1 (inorder t) \
  lookup t a = map_of (inorder t) a"
and inorder_update: "inv t \ sorted1 (inorder t) \
  inorder(update a b t) = upd_list a b (inorder t)"
and inorder_delete: "inv t \ sorted1 (inorder t) \
  inorder(delete a t) = del_list a (inorder t)"
and inorder_inv_empty:  "inv empty"
and inorder_inv_update: "inv t \ sorted1 (inorder t) \ inv(update a b t)"
and inorder_inv_delete: "inv t \ sorted1 (inorder t) \ inv(delete a t)"

begin

text \<open>It implements the traditional specification:\<close>

definition invar :: "'t \ bool" where
"invar t == inv t \ sorted1 (inorder t)"

sublocale Map
  empty update delete lookup invar
proof(standard, goal_cases)
  case 1 show ?case by (auto simp: inorder_lookup inorder_empty inorder_inv_empty)
next
  case 2 thus ?case
    by(simp add: fun_eq_iff inorder_update inorder_inv_update map_of_ins_list inorder_lookup
         sorted_upd_list invar_def)
next
  case 3 thus ?case
    by(simp add: fun_eq_iff inorder_delete inorder_inv_delete map_of_del_list inorder_lookup
         sorted_del_list invar_def)
next
  case 4 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
next
  case 5 thus ?case by(simp add: inorder_update inorder_inv_update sorted_upd_list invar_def)
next
  case 6 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
qed

end

end

quality69%

¤ 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.0.13Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.