Quelle HeapSyntax.thy Sprache: Isabelle

(*  Title:      HOL/Hoare/HeapSyntax.thy
    Author:     Tobias Nipkow
    Copyright   2002 TUM
*)

section \<open>Heap syntax\<close>

theory HeapSyntax
  imports Hoare_Logic Heap
begin

subsection "Field access and update"

syntax
  "_refupdate" :: "('a \ 'b) \ 'a ref \ 'b \ ('a \ 'b)"
    (\<open>(\<open>open_block notation=\<open>mixfix Hoare ref update\<close>\<close>_/'((_ \<rightarrow> _)'))\<close> [1000,0] 900)
  "_fassign"  :: "'a ref => id => 'v => 's com"
    (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare ref assignment\<close>\<close>_^._ :=/ _)\<close> [70,1000,65] 61)
  "_faccess"  :: "'a ref => ('a ref \ 'v) => 'v"
    (\<open>(\<open>open_block notation=\<open>infix Hoare ref access\<close>\<close>_^._)\<close> [65,1000] 65)
translations
  "f(r \ v)" == "f(CONST addr r := v)"
  "p^.f := e" => "f := f(p \ e)"
  "p^.f" => "f(CONST addr p)"

declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]

text "An example due to Suzuki:"

lemma "VARS v n
  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
   distinct[w0,x0,y0,z0]}
  w^.v := (1::int); w^.n := x;
  x^.v := 2; x^.n := y;
  y^.v := 3; y^.n := z;
  z^.v := 4; x^.n := z
  {w^.n^.n^.v = 4}"
by vcg_simp

end

quality98%

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