1.1 --- a/src/HOL/IsaMakefile Wed Jun 13 16:30:12 2001 +0200
1.2 +++ b/src/HOL/IsaMakefile Sat Jun 16 20:06:42 2001 +0200
1.3 @@ -31,6 +31,7 @@
1.4 HOL-MicroJava \
1.5 HOL-MiniML \
1.6 HOL-Modelcheck \
1.7 + HOL-NanoJava \
1.8 HOL-NumberTheory \
1.9 HOL-Prolog \
1.10 HOL-Subst \
1.11 @@ -460,6 +461,15 @@
1.12 MicroJava/document/root.bib MicroJava/document/root.tex
1.13 @$(ISATOOL) usedir $(OUT)/HOL MicroJava
1.14
1.15 +## HOL-NanoJava
1.16 +
1.17 +HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
1.18 +
1.19 +$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
1.20 + NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
1.21 + NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
1.22 + NanoJava/document/root.bib NanoJava/document/root.tex
1.23 + @$(ISATOOL) usedir $(OUT)/HOL NanoJava
1.24
1.25 ## HOL-CTL
1.26
1.27 @@ -581,7 +591,7 @@
1.28 ## clean
1.29
1.30 clean:
1.31 - @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
1.32 + @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
1.33 $(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
1.34 $(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
1.35 $(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
1.36 @@ -589,8 +599,8 @@
1.37 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
1.38 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
1.39 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
1.40 - $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
1.41 - $(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
1.42 + $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-CTL.gz \
1.43 + $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
1.44 $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
1.45 $(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
1.46 $(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/NanoJava/AxSem.thy Sat Jun 16 20:06:42 2001 +0200
2.3 @@ -0,0 +1,122 @@
2.4 +(* Title: HOL/NanoJava/AxSem.thy
2.5 + ID: $Id$
2.6 + Author: David von Oheimb
2.7 + Copyright 2001 Technische Universitaet Muenchen
2.8 +*)
2.9 +
2.10 +header "Axiomatic Semantics (Hoare Logic)"
2.11 +
2.12 +theory AxSem = State:
2.13 +
2.14 +types assn = "state => bool"
2.15 + triple = "assn \<times> stmt \<times> assn"
2.16 +translations
2.17 + "assn" \<leftharpoondown> (type)"state => bool"
2.18 + "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
2.19 +
2.20 +consts hoare :: "(triple set \<times> triple set) set"
2.21 +syntax (xsymbols)
2.22 + "@hoare" :: "[triple set, triple set ] => bool" ("_ |\<turnstile>/ _" [61,61] 60)
2.23 + "@hoare1" :: "[triple set, assn,stmt,assn] => bool"
2.24 + ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
2.25 +syntax
2.26 + "@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60)
2.27 + "@hoare1" :: "[triple set, assn,stmt,assn] => bool"
2.28 + ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
2.29 +
2.30 +translations "A |\<turnstile> C" \<rightleftharpoons> "(A,C) \<in> hoare"
2.31 + "A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
2.32 +
2.33 +inductive hoare
2.34 +intros
2.35 +
2.36 + Skip: "A |- {P} Skip {P}"
2.37 +
2.38 + Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
2.39 +
2.40 + Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q};
2.41 + A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q} |] ==>
2.42 + A |- {P} If(e) c1 Else c2 {Q}"
2.43 +
2.44 + Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
2.45 + A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
2.46 +
2.47 + NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
2.48 + x:=new C {P}"
2.49 +
2.50 + Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
2.51 + P (lupd(x|->s<y>) s)} x:=(C)y {P}"
2.52 +
2.53 + FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
2.54 +
2.55 + FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
2.56 +
2.57 + Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and>
2.58 + s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
2.59 + Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
2.60 + A |- {P} x:={C}y..m(p) {Q}"
2.61 +
2.62 + Meth: "\<forall>D. A |- {\<lambda>s. \<exists>a. s<This> = Addr a \<and> D=obj_class s a \<and> D <=C C \<and> P s}
2.63 + Impl D m {Q} ==>
2.64 + A |- {P} Meth C m {Q}"
2.65 +
2.66 + (*\<Union>z instead of \<forall>z in the conclusion and
2.67 + z restricted to type state due to limitations of the inductive paackage *)
2.68 + Impl: "A\<union> (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||-
2.69 + (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
2.70 + A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
2.71 +
2.72 +(* structural rules *)
2.73 +
2.74 + (* z restricted to type state due to limitations of the inductive paackage *)
2.75 + Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
2.76 + \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
2.77 + A |- {P} c {Q }"
2.78 +
2.79 + Asm: " a \<in> A ==> A ||- {a}"
2.80 +
2.81 + ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
2.82 +
2.83 + ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
2.84 +
2.85 +
2.86 +subsection "Derived Rules"
2.87 +
2.88 +lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
2.89 +apply (rule hoare.Conseq)
2.90 +apply (rule allI, assumption)
2.91 +apply fast
2.92 +done
2.93 +
2.94 +lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
2.95 +apply (rule hoare.ConjI)
2.96 +apply clarify
2.97 +apply (drule hoare.ConjE)
2.98 +apply fast
2.99 +apply assumption
2.100 +done
2.101 +
2.102 +lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
2.103 +by (auto intro: hoare.ConjI hoare.ConjE)
2.104 +
2.105 +lemma Impl':
2.106 + "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
2.107 + (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
2.108 + A ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
2.109 +apply (drule Union[THEN iffD2])
2.110 +apply (drule hoare.Impl)
2.111 +apply (drule Union[THEN iffD1])
2.112 +apply (erule spec)
2.113 +done
2.114 +
2.115 +lemma Impl1:
2.116 + "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
2.117 + (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms;
2.118 + (C,m)\<in> ms\<rbrakk> \<Longrightarrow>
2.119 + A \<turnstile> {P z C m} Impl C m {Q (z::state) C m}"
2.120 +apply (drule Impl')
2.121 +apply (erule Weaken)
2.122 +apply (auto del: image_eqI intro: rev_image_eqI)
2.123 +done
2.124 +
2.125 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/NanoJava/Decl.thy Sat Jun 16 20:06:42 2001 +0200
3.3 @@ -0,0 +1,68 @@
3.4 +(* Title: HOL/NanoJava/Decl.thy
3.5 + ID: $Id$
3.6 + Author: David von Oheimb
3.7 + Copyright 2001 Technische Universitaet Muenchen
3.8 +*)
3.9 +
3.10 +header "Types, class Declarations, and whole programs"
3.11 +
3.12 +theory Decl = Term:
3.13 +
3.14 +datatype ty
3.15 + = NT (* null type *)
3.16 + | Class cname (* class type *)
3.17 +
3.18 +types fdecl (* field declaration *)
3.19 + = "vnam \<times> ty"
3.20 +
3.21 +
3.22 +record methd (* method declaration *)
3.23 + = par :: ty
3.24 + res :: ty
3.25 + lcl ::"(vname \<times> ty) list"
3.26 + bdy :: stmt
3.27 +
3.28 +types mdecl (* method declaration *)
3.29 + = "mname \<times> methd"
3.30 +
3.31 +record class (* class *)
3.32 + = super :: cname
3.33 + fields ::"fdecl list"
3.34 + methods ::"mdecl list"
3.35 +
3.36 +types cdecl (* class declaration *)
3.37 + = "cname \<times> class"
3.38 +
3.39 +types prog
3.40 + = "cdecl list"
3.41 +
3.42 +translations
3.43 + "fdecl" \<leftharpoondown> (type)"vname \<times> ty"
3.44 + "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
3.45 + "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
3.46 + "cdecl" \<leftharpoondown> (type)"cname \<times> class"
3.47 + "prog " \<leftharpoondown> (type)"cdecl list"
3.48 +
3.49 +consts
3.50 +
3.51 + Prog :: prog (* program as a global value *)
3.52 +
3.53 +consts
3.54 +
3.55 + Object :: cname (* name of root class *)
3.56 +
3.57 +
3.58 +constdefs
3.59 + class :: "cname \<leadsto> class"
3.60 + "class \<equiv> map_of Prog"
3.61 +
3.62 + is_class :: "cname => bool"
3.63 + "is_class C \<equiv> class C \<noteq> None"
3.64 +
3.65 +lemma finite_is_class: "finite {C. is_class C}"
3.66 +apply (unfold is_class_def class_def)
3.67 +apply (fold dom_def)
3.68 +apply (rule finite_dom_map_of)
3.69 +done
3.70 +
3.71 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/NanoJava/Equivalence.thy Sat Jun 16 20:06:42 2001 +0200
4.3 @@ -0,0 +1,237 @@
4.4 +(* Title: HOL/NanoJava/Equivalence.thy
4.5 + ID: $Id$
4.6 + Author: David von Oheimb
4.7 + Copyright 2001 Technische Universitaet Muenchen
4.8 +*)
4.9 +
4.10 +header "Equivalence of Operational and Axiomatic Semantics"
4.11 +
4.12 +theory Equivalence = OpSem + AxSem:
4.13 +
4.14 +subsection "Validity"
4.15 +
4.16 +constdefs
4.17 + valid :: "[assn,stmt,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
4.18 + "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c-n-> t) --> Q t"
4.19 +
4.20 + nvalid :: "[nat, triple ] => bool" ("|=_: _" [61,61] 60)
4.21 + "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c-n-> t --> P s --> Q t"
4.22 +
4.23 + nvalids :: "[nat, triple set] => bool" ("||=_: _" [61,61] 60)
4.24 + "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
4.25 +
4.26 + cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"[61,61] 60)
4.27 + "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
4.28 +
4.29 +syntax (xsymbols)
4.30 + valid :: "[assn,stmt,assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
4.31 + nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60)
4.32 + nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60)
4.33 + cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
4.34 +
4.35 +syntax
4.36 + nvalid1::"[nat, assn,stmt,assn] => bool" ( "|=_:.{(1_)}/ (_)/ {(1_)}"
4.37 + [61,3,90,3] 60)
4.38 + cnvalid1::"[triple set, assn,stmt,assn] => bool" ("_ ||=.{(1_)}/ (_)/ {(1_)}"
4.39 + [61,3,90,3] 60)
4.40 +syntax (xsymbols)
4.41 + nvalid1::"[nat, assn,stmt,assn] => bool" ( "\<Turnstile>_:.{(1_)}/ (_)/ {(1_)}"
4.42 + [61,3,90,3] 60)
4.43 + cnvalid1::"[triple set, assn,stmt,assn] => bool" ( "_ |\<Turnstile>.{(1_)}/ (_)/ {(1_)}"
4.44 + [61,3,90,3] 60)
4.45 +translations
4.46 + " \<Turnstile>n:.{P} c {Q}" \<rightleftharpoons> " \<Turnstile>n: (P,c,Q)"
4.47 + "A |\<Turnstile>.{P} c {Q}" \<rightleftharpoons> "A |\<Turnstile> {(P,c,Q)}"
4.48 +
4.49 +lemma nvalid1_def2: "\<Turnstile>n:.{P} c {Q} \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
4.50 +by (simp add: nvalid_def Let_def)
4.51 +
4.52 +lemma cnvalid1_def2:
4.53 + "A |\<Turnstile>.{P} c {Q} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
4.54 +by(simp add: nvalid1_def2 nvalids_def cnvalids_def)
4.55 +
4.56 +lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n:.{P} c {Q})"
4.57 +apply (simp add: valid_def nvalid1_def2)
4.58 +apply blast
4.59 +done
4.60 +
4.61 +
4.62 +subsection "Soundness"
4.63 +
4.64 +declare exec_elim_cases [elim!]
4.65 +
4.66 +lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
4.67 +by (clarsimp simp add: nvalid1_def2)
4.68 +
4.69 +lemma Impl_nvalid_Suc: "\<Turnstile>n:.{P} body C m {Q} \<Longrightarrow> \<Turnstile>Suc n:.{P} Impl C m {Q}"
4.70 +by (clarsimp simp add: nvalid1_def2)
4.71 +
4.72 +lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
4.73 +by (force simp add: split_paired_all nvalid1_def2 intro: exec_mono)
4.74 +
4.75 +lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow> Ball A (nvalid n)"
4.76 +by (fast intro: nvalid_SucD)
4.77 +
4.78 +lemma Loop_sound_lemma [rule_format (no_asm)]:
4.79 +"\<lbrakk>\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<e> \<noteq> Null \<longrightarrow> P t; s -c0-n0\<rightarrow> t\<rbrakk> \<Longrightarrow>
4.80 + P s \<longrightarrow> c0 = While (e) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<e> = Null"
4.81 +apply (erule exec.induct)
4.82 +apply clarsimp+
4.83 +done
4.84 +
4.85 +lemma Impl_sound_lemma:
4.86 +"\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
4.87 + (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
4.88 +by blast
4.89 +
4.90 +lemma hoare_sound_main: "A |\<turnstile> C \<Longrightarrow> A |\<Turnstile> C"
4.91 +apply (erule hoare.induct)
4.92 +apply (simp_all only: cnvalid1_def2)
4.93 +apply clarsimp
4.94 +apply clarsimp
4.95 +apply (clarsimp split add: split_if_asm)
4.96 +apply (clarsimp,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
4.97 +apply clarsimp
4.98 +apply clarsimp
4.99 +apply clarsimp
4.100 +apply clarsimp
4.101 +apply (clarsimp del: Meth_elim_cases) (* Call *)
4.102 +apply (clarsimp del: Impl_elim_cases) (* Meth *)
4.103 +defer
4.104 +apply blast (* Conseq *)
4.105 +apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
4.106 +apply blast
4.107 +apply blast
4.108 +apply blast
4.109 +(* Impl *)
4.110 +apply (erule thin_rl)
4.111 +apply (rule allI)
4.112 +apply (induct_tac "n")
4.113 +apply (clarify intro!: Impl_nvalid_0)
4.114 +apply (clarify intro!: Impl_nvalid_Suc)
4.115 +apply (drule nvalids_SucD)
4.116 +apply (erule (1) impE)
4.117 +apply (drule (4) Impl_sound_lemma)
4.118 +done
4.119 +
4.120 +theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
4.121 +apply (simp only: valid_def2)
4.122 +apply (drule hoare_sound_main)
4.123 +apply (unfold cnvalids_def nvalids_def)
4.124 +apply fast
4.125 +done
4.126 +
4.127 +
4.128 +subsection "(Relative) Completeness"
4.129 +
4.130 +constdefs MGT :: "stmt => state => triple"
4.131 + "MGT c z \<equiv> (\<lambda> s. z = s, c, %t. \<exists>n. z -c-n-> t)"
4.132 +
4.133 +lemma MGF_implies_complete:
4.134 + "\<forall>z. {} |\<turnstile> {MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
4.135 +apply (simp only: valid_def2)
4.136 +apply (unfold MGT_def)
4.137 +apply (erule hoare.Conseq)
4.138 +apply (clarsimp simp add: nvalid1_def2)
4.139 +done
4.140 +
4.141 +
4.142 +declare exec.intros[intro!]
4.143 +
4.144 +lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow>
4.145 + A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
4.146 +apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
4.147 + in hoare.Conseq)
4.148 +apply (rule allI)
4.149 +apply (rule hoare.Loop)
4.150 +apply (erule hoare.Conseq)
4.151 +apply clarsimp
4.152 +apply (blast intro:rtrancl_into_rtrancl)
4.153 +apply (erule thin_rl)
4.154 +apply clarsimp
4.155 +apply (erule_tac x = z in allE)
4.156 +apply clarsimp
4.157 +apply (erule converse_rtrancl_induct)
4.158 +apply blast
4.159 +apply clarsimp
4.160 +apply (drule (1) exec_max2)
4.161 +apply (blast del: exec_elim_cases)
4.162 +done
4.163 +
4.164 +lemma MGF_lemma[rule_format]:
4.165 + "(\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z}) \<longrightarrow> (\<forall>z. A |\<turnstile> {MGT c z})"
4.166 +apply (simp add: MGT_def)
4.167 +apply (induct_tac c)
4.168 +apply (tactic "ALLGOALS Clarify_tac")
4.169 +
4.170 +apply (rule Conseq1 [OF hoare.Skip])
4.171 +apply blast
4.172 +
4.173 +apply (rule hoare.Comp)
4.174 +apply (erule spec)
4.175 +apply (erule hoare.Conseq)
4.176 +apply (erule thin_rl, erule thin_rl)
4.177 +apply clarsimp
4.178 +apply (drule (1) exec_max2)
4.179 +apply blast
4.180 +
4.181 +apply (rule hoare.Cond)
4.182 +apply (erule hoare.Conseq)
4.183 +apply (erule thin_rl, erule thin_rl)
4.184 +apply force
4.185 +apply (erule hoare.Conseq)
4.186 +apply (erule thin_rl, erule thin_rl)
4.187 +apply force
4.188 +
4.189 +apply (erule MGF_Loop)
4.190 +
4.191 +apply (rule Conseq1 [OF hoare.NewC])
4.192 +apply blast
4.193 +
4.194 +apply (rule Conseq1 [OF hoare.Cast])
4.195 +apply blast
4.196 +
4.197 +apply (rule Conseq1 [OF hoare.FAcc])
4.198 +apply blast
4.199 +
4.200 +apply (rule Conseq1 [OF hoare.FAss])
4.201 +apply blast
4.202 +
4.203 +apply (rule hoare.Call)
4.204 +apply (rule allI)
4.205 +apply (rule hoare.Meth)
4.206 +apply (rule allI)
4.207 +apply (drule spec, drule spec, erule hoare.Conseq)
4.208 +apply blast
4.209 +
4.210 +apply (rule hoare.Meth)
4.211 +apply (rule allI)
4.212 +apply (drule spec, drule spec, erule hoare.Conseq)
4.213 +apply blast
4.214 +
4.215 +apply blast
4.216 +done
4.217 +
4.218 +lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
4.219 +apply (unfold MGT_def)
4.220 +apply (rule Impl1)
4.221 +apply (rule_tac [2] UNIV_I)
4.222 +apply clarsimp
4.223 +apply (rule hoare.ConjI)
4.224 +apply clarsimp
4.225 +apply (rule ssubst [OF Impl_body_eq])
4.226 +apply (fold MGT_def)
4.227 +apply (rule MGF_lemma)
4.228 +apply (rule hoare.Asm)
4.229 +apply force
4.230 +done
4.231 +
4.232 +theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
4.233 +apply (rule MGF_implies_complete)
4.234 +apply (erule_tac [2] asm_rl)
4.235 +apply (rule allI)
4.236 +apply (rule MGF_lemma)
4.237 +apply (rule MGF_Impl)
4.238 +done
4.239 +
4.240 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/NanoJava/OpSem.thy Sat Jun 16 20:06:42 2001 +0200
5.3 @@ -0,0 +1,89 @@
5.4 +(* Title: HOL/NanoJava/OpSem.thy
5.5 + ID: $Id$
5.6 + Author: David von Oheimb
5.7 + Copyright 2001 Technische Universitaet Muenchen
5.8 +*)
5.9 +
5.10 +header "Operational Evaluation Semantics"
5.11 +
5.12 +theory OpSem = State:
5.13 +
5.14 +consts
5.15 + exec :: "(state \<times> stmt \<times> nat \<times> state) set"
5.16 +syntax (xsymbols)
5.17 + exec :: "[state, stmt, nat, state] => bool" ("_ -_-_\<rightarrow> _" [98,90,99,98] 89)
5.18 +syntax
5.19 + exec :: "[state, stmt, nat, state] => bool" ("_ -_-_-> _" [98,90,99,98] 89)
5.20 +translations
5.21 + "s -c-n-> s'" == "(s, c, n, s') \<in> exec"
5.22 +
5.23 +inductive exec intros
5.24 +
5.25 + Skip: " s -Skip-n-> s"
5.26 +
5.27 + Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
5.28 + s0 -c1;; c2-n-> s2"
5.29 +
5.30 + Cond: "[| s -(if s<e> \<noteq> Null then c1 else c2)-n-> s' |] ==>
5.31 + s -If(e) c1 Else c2-n-> s'"
5.32 +
5.33 + LoopF:" s0<e> = Null ==>
5.34 + s0 -While(e) c-n-> s0"
5.35 + LoopT:"[| s0<e> \<noteq> Null; s0 -c-n-> s1; s1 -While(e) c-n-> s2 |] ==>
5.36 + s0 -While(e) c-n-> s2"
5.37 +
5.38 + NewC: " new_Addr s = Addr a ==>
5.39 + s -x:=new C-n-> lupd(x\<mapsto>Addr a)(new_obj a C s)"
5.40 +
5.41 + Cast: " (case s<y> of Null => True | Addr a => obj_class s a \<preceq>C C) ==>
5.42 + s -x:=(C)y-n-> lupd(x\<mapsto>s<y>) s"
5.43 +
5.44 + FAcc: " s<y> = Addr a ==>
5.45 + s -x:=y..f-n-> lupd(x\<mapsto>get_field s a f) s"
5.46 +
5.47 + FAss: " s<y> = Addr a ==>
5.48 + s -y..f:=x-n-> upd_obj a f (s<x>) s"
5.49 +
5.50 + Call: "lupd(This\<mapsto>s<y>)(lupd(Param\<mapsto>s<p>)(init_locs C m s))-Meth C m -n-> s'==>
5.51 + s -x:={C}y..m(p)-n-> lupd(x\<mapsto>s'<Res>)(set_locs s s')"
5.52 +
5.53 + Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
5.54 + s -Impl (obj_class s a) m-n-> s' |] ==>
5.55 + s -Meth C m-n-> s'"
5.56 +
5.57 + Impl: " s -body C m- n-> s' ==>
5.58 + s -Impl C m-Suc n-> s'"
5.59 +
5.60 +inductive_cases exec_elim_cases':
5.61 + "s -Skip -n-> t"
5.62 + "s -c1;; c2 -n-> t"
5.63 + "s -If(e) c1 Else c2-n-> t"
5.64 + "s -While(e) c -n-> t"
5.65 + "s -x:=new C -n-> t"
5.66 + "s -x:=(C)y -n-> t"
5.67 + "s -x:=y..f -n-> t"
5.68 + "s -y..f:=x -n-> t"
5.69 + "s -x:={C}y..m(p) -n-> t"
5.70 +inductive_cases Meth_elim_cases: "s -Meth C m -n-> t"
5.71 +inductive_cases Impl_elim_cases: "s -Impl C m -n-> t"
5.72 +lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
5.73 +
5.74 +lemma exec_mono [rule_format]: "s -c-n\<rightarrow> t \<Longrightarrow> \<forall>m. n \<le> m \<longrightarrow> s -c-m\<rightarrow> t"
5.75 +apply (erule exec.induct)
5.76 +prefer 12 (* Impl *)
5.77 +apply clarify
5.78 +apply (rename_tac n)
5.79 +apply (case_tac n)
5.80 +apply (blast intro:exec.intros)+
5.81 +done
5.82 +
5.83 +lemma exec_max2: "\<lbrakk>s1 -c1- n1 \<rightarrow> t1 ; s2 -c2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow>
5.84 + s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
5.85 +by (fast intro: exec_mono le_maxI1 le_maxI2)
5.86 +
5.87 +lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl C m-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body C m-n\<rightarrow> t)"
5.88 +apply (rule ext)
5.89 +apply (fast elim: exec_elim_cases intro: exec.Impl)
5.90 +done
5.91 +
5.92 +end
5.93 \ No newline at end of file
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/NanoJava/ROOT.ML Sat Jun 16 20:06:42 2001 +0200
6.3 @@ -0,0 +1,1 @@
6.4 +use_thy "Equivalence";
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/NanoJava/State.thy Sat Jun 16 20:06:42 2001 +0200
7.3 @@ -0,0 +1,111 @@
7.4 +(* Title: HOL/NanoJava/State.thy
7.5 + ID: $Id$
7.6 + Author: David von Oheimb
7.7 + Copyright 2001 Technische Universitaet Muenchen
7.8 +*)
7.9 +
7.10 +header "Program State"
7.11 +
7.12 +theory State = TypeRel:
7.13 +
7.14 +constdefs
7.15 +
7.16 + body :: "cname => mname => stmt"
7.17 + "body C m \<equiv> bdy (the (method C m))"
7.18 +
7.19 +text {* locations, i.e.\ abstract references to objects *}
7.20 +typedecl loc
7.21 +arities loc :: "term"
7.22 +
7.23 +datatype val
7.24 + = Null (* null reference *)
7.25 + | Addr loc (* address, i.e. location of object *)
7.26 +
7.27 +types fields
7.28 + = "(vnam \<leadsto> val)"
7.29 +
7.30 + obj = "cname \<times> fields"
7.31 +
7.32 +translations
7.33 +
7.34 + "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option"
7.35 + "obj" \<leftharpoondown> (type)"cname \<times> fields"
7.36 +
7.37 +constdefs
7.38 +
7.39 + init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
7.40 + "init_vars m == option_map (\<lambda>T. Null) o m"
7.41 +
7.42 +text {* private *}
7.43 +types heap = "loc \<leadsto> obj"
7.44 + locals = "vname \<leadsto> val"
7.45 +
7.46 +text {* private *}
7.47 +record state
7.48 + = heap :: heap
7.49 + locals :: locals
7.50 +
7.51 +translations
7.52 +
7.53 + "heap" \<leftharpoondown> (type)"loc => obj option"
7.54 + "locals" \<leftharpoondown> (type)"vname => val option"
7.55 + "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
7.56 +
7.57 +constdefs
7.58 +
7.59 + init_locs :: "cname => mname => state => state"
7.60 + "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m))))|)"
7.61 +
7.62 +text {* The first parameter of @{term set_locs} is of type @{typ state}
7.63 + rather than @{typ locals} in order to keep @{typ locals} private.*}
7.64 +constdefs
7.65 + set_locs :: "state => state => state"
7.66 + "set_locs s s' \<equiv> s' (| locals := locals s |)"
7.67 +
7.68 + get_local :: "state => vname => val" ("_<_>" [99,0] 99)
7.69 + "get_local s x \<equiv> the (locals s x)"
7.70 +
7.71 +(* local function: *)
7.72 + get_obj :: "state => loc => obj"
7.73 + "get_obj s a \<equiv> the (heap s a)"
7.74 +
7.75 + obj_class :: "state => loc => cname"
7.76 + "obj_class s a \<equiv> fst (get_obj s a)"
7.77 +
7.78 + get_field :: "state => loc => vnam => val"
7.79 + "get_field s a f \<equiv> the (snd (get_obj s a) f)"
7.80 +
7.81 +constdefs
7.82 +
7.83 +(* local function: *)
7.84 + hupd :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state" ("hupd'(_|->_')" [10,10] 1000)
7.85 + "hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)"
7.86 +
7.87 + lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000)
7.88 + "lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)"
7.89 +
7.90 +syntax (xsymbols)
7.91 + hupd :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state" ("hupd'(_\<mapsto>_')" [10,10] 1000)
7.92 + lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
7.93 +
7.94 +constdefs
7.95 +
7.96 + new_obj :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state"
7.97 + "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
7.98 +
7.99 + upd_obj :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
7.100 + "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"
7.101 +
7.102 + new_Addr :: "state => val"
7.103 + "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"
7.104 +
7.105 +lemma new_AddrD:
7.106 +"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null"
7.107 +apply (unfold new_Addr_def)
7.108 +apply (erule subst)
7.109 +apply (rule someI)
7.110 +apply (rule disjI2)
7.111 +apply (rule HOL.refl)
7.112 +done
7.113 +
7.114 +end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/NanoJava/Term.thy Sat Jun 16 20:06:42 2001 +0200
8.3 @@ -0,0 +1,46 @@
8.4 +(* Title: HOL/NanoJava/Term.thy
8.5 + ID: $Id$
8.6 + Author: David von Oheimb
8.7 + Copyright 2001 Technische Universitaet Muenchen
8.8 +*)
8.9 +
8.10 +header "Statements and expression emulations"
8.11 +
8.12 +theory Term = Main:
8.13 +
8.14 +typedecl cname (* class name *)
8.15 +typedecl vnam (* variable or field name *)
8.16 +typedecl mname (* method name *)
8.17 +arities cname :: "term"
8.18 + vnam :: "term"
8.19 + mname :: "term"
8.20 +
8.21 +datatype vname (* variable for special names *)
8.22 + = This (* This pointer *)
8.23 + | Param (* method parameter *)
8.24 + | Res (* method result *)
8.25 + | VName vnam
8.26 +
8.27 +datatype stmt
8.28 + = Skip (* empty statement *)
8.29 + | Comp stmt stmt ("_;; _" [91,90] 90)
8.30 + | Cond vname stmt stmt ("If '(_') _ Else _" [99,91,91] 91)
8.31 + | Loop vname stmt ("While '(_') _" [99,91 ] 91)
8.32 +
8.33 + | NewC vname cname ("_:=new _" [99, 99] 95) (* object creation *)
8.34 + | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
8.35 + | FAcc vname vname vnam ("_:=_.._" [99,99,99] 95) (* field access *)
8.36 + | FAss vname vnam vname ("_.._:=_" [99,99,99] 95) (* field assigment *)
8.37 + | Call vname cname vname mname vname (* method call *)
8.38 + ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
8.39 + | Meth cname mname (* virtual method *)
8.40 + | Impl cname mname (* method implementation *)
8.41 +
8.42 +(*###TO Product_Type_lemmas.ML*)
8.43 +lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
8.44 +apply (rule_tac x = "(a,b)" in image_eqI)
8.45 +apply auto
8.46 +done
8.47 +
8.48 +end
8.49 +
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/NanoJava/TypeRel.thy Sat Jun 16 20:06:42 2001 +0200
9.3 @@ -0,0 +1,145 @@
9.4 +(* Title: HOL/NanoJava/TypeRel.thy
9.5 + ID: $Id$
9.6 + Author: David von Oheimb
9.7 + Copyright 2001 Technische Universitaet Muenchen
9.8 +*)
9.9 +
9.10 +header "Type relations"
9.11 +
9.12 +theory TypeRel = Decl:
9.13 +
9.14 +consts
9.15 + widen :: "(ty \<times> ty ) set" (* widening *)
9.16 + subcls1 :: "(cname \<times> cname) set" (* subclass *)
9.17 +
9.18 +syntax (xsymbols)
9.19 + widen :: "[ty , ty ] => bool" ("_ \<preceq> _" [71,71] 70)
9.20 + subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70)
9.21 + subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70)
9.22 +syntax
9.23 + widen :: "[ty , ty ] => bool" ("_ <= _" [71,71] 70)
9.24 + subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
9.25 + subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
9.26 +
9.27 +translations
9.28 + "C \<prec>C1 D" == "(C,D) \<in> subcls1"
9.29 + "C \<preceq>C D" == "(C,D) \<in> subcls1^*"
9.30 + "S \<preceq> T" == "(S,T) \<in> widen"
9.31 +
9.32 +consts
9.33 + method :: "cname => (mname \<leadsto> methd)"
9.34 + field :: "cname => (vnam \<leadsto> ty)"
9.35 +
9.36 +
9.37 +text {* The rest of this theory is not actually used. *}
9.38 +
9.39 +defs
9.40 + (* direct subclass relation *)
9.41 + subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
9.42 +
9.43 +inductive widen intros (*widening, viz. method invocation conversion,
9.44 + i.e. sort of syntactic subtyping *)
9.45 + refl [intro!, simp]: "T \<preceq> T"
9.46 + subcls : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
9.47 + null [intro!]: "NT \<preceq> R"
9.48 +
9.49 +lemma subcls1D:
9.50 + "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
9.51 +apply (unfold subcls1_def)
9.52 +apply auto
9.53 +done
9.54 +
9.55 +lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D"
9.56 +apply (unfold subcls1_def)
9.57 +apply auto
9.58 +done
9.59 +
9.60 +lemma subcls1_def2:
9.61 +"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
9.62 +apply (unfold subcls1_def is_class_def)
9.63 +apply auto
9.64 +done
9.65 +
9.66 +lemma finite_subcls1: "finite subcls1"
9.67 +apply(subst subcls1_def2)
9.68 +apply(rule finite_SigmaI [OF finite_is_class])
9.69 +apply(rule_tac B = "{super (the (class C))}" in finite_subset)
9.70 +apply auto
9.71 +done
9.72 +
9.73 +constdefs
9.74 +
9.75 + ws_prog :: "bool"
9.76 + "ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow>
9.77 + is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
9.78 +
9.79 +lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow>
9.80 + is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
9.81 +apply (unfold ws_prog_def class_def)
9.82 +apply (drule_tac map_of_SomeD)
9.83 +apply auto
9.84 +done
9.85 +
9.86 +lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
9.87 +by (fast dest: subcls1D ws_progD)
9.88 +
9.89 +(* context (theory "Transitive_Closure") *)
9.90 +lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
9.91 +apply (rule allI)
9.92 +apply (erule irrefl_tranclI)
9.93 +done
9.94 +
9.95 +lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
9.96 +
9.97 +lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y"
9.98 +apply (rule irrefl_trancl_rD)
9.99 +apply (rule subcls1_irrefl_lemma2)
9.100 +apply auto
9.101 +done
9.102 +
9.103 +lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
9.104 +
9.105 +lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
9.106 +by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
9.107 +
9.108 +
9.109 +consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
9.110 +
9.111 +recdef class_rec "subcls1\<inverse>"
9.112 + "class_rec C = (\<lambda>f. case class C of None \<Rightarrow> arbitrary
9.113 + | Some m \<Rightarrow> if wf (subcls1\<inverse>)
9.114 + then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
9.115 + else arbitrary)"
9.116 +(hints intro: subcls1I)
9.117 +
9.118 +lemma class_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
9.119 + class_rec C f = (if C = Object then empty else class_rec (super m) f) ++
9.120 + map_of (f m)";
9.121 +apply (drule wf_subcls1)
9.122 +apply (rule class_rec.simps [THEN trans [THEN fun_cong]])
9.123 +apply assumption
9.124 +apply simp
9.125 +done
9.126 +
9.127 +(* methods of a class, with inheritance and hiding *)
9.128 +defs method_def: "method C \<equiv> class_rec C methods"
9.129 +
9.130 +lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
9.131 +method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
9.132 +apply (unfold method_def)
9.133 +apply (erule (1) class_rec [THEN trans]);
9.134 +apply simp
9.135 +done
9.136 +
9.137 +
9.138 +(* fields of a class, with inheritance and hiding *)
9.139 +defs field_def: "field C \<equiv> class_rec C fields"
9.140 +
9.141 +lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
9.142 +field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
9.143 +apply (unfold field_def)
9.144 +apply (erule (1) class_rec [THEN trans]);
9.145 +apply simp
9.146 +done
9.147 +
9.148 +end
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/NanoJava/document/root.bib Sat Jun 16 20:06:42 2001 +0200
10.3 @@ -0,0 +1,58 @@
10.4 +@inproceedings{NipkowOP00,
10.5 + author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
10.6 + title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
10.7 + booktitle = {Foundations of Secure Computation},
10.8 + series= {NATO Science Series F: Computer and Systems Sciences},
10.9 + volume = {175},
10.10 + year = {2000},
10.11 + publisher = {IOS Press},
10.12 + editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
10.13 + abstract = {This paper introduces the subset $micro$Java of Java,
10.14 +essentially by omitting everything but classes.
10.15 +The type system and semantics of this language
10.16 +(and a corresponding abstract Machine $micro$JVM)
10.17 +are formalized in the theorem prover Isabelle/HOL.
10.18 +Type safety both of $micro$Java and the $micro$JVM
10.19 +are mechanically verified.
10.20 +
10.21 +To make the paper self-contained, it starts with
10.22 +introductions to Isabelle/HOL and the art of
10.23 +embedding languages in theorem provers.},
10.24 + CRClassification = {D.3.1, F.3.2},
10.25 + CRGenTerms = {Languages, Reliability, Theory, Verification},
10.26 + url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
10.27 + pages = {117--144}
10.28 +}
10.29 +
10.30 +
10.31 +@article{DvO-CPE01,
10.32 + author = {David von Oheimb},
10.33 + title = {Hoare Logic for {J}ava in {Isabelle/HOL}},
10.34 + journal = {Concurrency: Practice and Experience},
10.35 + year = {2001},
10.36 + url = {http://www4.in.tum.de/papers/DvO-CPE01.html},
10.37 + abstract = {
10.38 +This article presents a Hoare-style calculus for a substantial subset
10.39 +of Java Card, which we call Java_light. In particular, the language
10.40 +includes side-effecting expressions, mutual recursion, dynamic method
10.41 +binding, full exception handling, and static class initialization.
10.42 +
10.43 +The Hoare logic of partial correctness is proved not only sound (w.r.t.
10.44 +our operational semantics of Java_light, described in detail elsewhere)
10.45 +but even complete. It is the first logic for an object-oriented
10.46 +language that is provably complete.
10.47 +The completeness proof uses a refinement of the Most General Formula
10.48 +approach. The proof of soundness gives new insights into the role of
10.49 +type safety. Further by-products of this work are a new general
10.50 +methodology for handling side-effecting expressions and their results,
10.51 +the discovery of the strongest possible rule of consequence, and a
10.52 +flexible Call rule for mutual recursion.
10.53 +We also give a small but non-trivial application example.
10.54 +
10.55 +All definitions and proofs have been done formally with the interactive
10.56 +theorem prover Isabelle/HOL. This guarantees not only rigorous definitions,
10.57 +but also gives maximal confidence in the results obtained.},
10.58 + CRClassification = {D.2.4, D.3.1, F.3.1},
10.59 + CRGenTerms = {Languages, Verification, Theory},
10.60 + note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
10.61 +}
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/NanoJava/document/root.tex Sat Jun 16 20:06:42 2001 +0200
11.3 @@ -0,0 +1,57 @@
11.4 +\documentclass[11pt,a4paper]{article}
11.5 +\usepackage{latexsym,isabelle,isabellesym,latexsym,pdfsetup}
11.6 +
11.7 +\urlstyle{tt}
11.8 +\pagestyle{myheadings}
11.9 +
11.10 +\addtolength{\hoffset}{-1,5cm}
11.11 +\addtolength{\textwidth}{4cm}
11.12 +\addtolength{\voffset}{-2cm}
11.13 +\addtolength{\textheight}{4cm}
11.14 +
11.15 +%subsection instead of section to make the toc readable
11.16 +\renewcommand{\thesubsection}{\arabic{subsection}}
11.17 +\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
11.18 +\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
11.19 +
11.20 +%remove spaces from the isabelle environment (trivlist makes them too large)
11.21 +\renewenvironment{isabelle}
11.22 +{\begin{isabellebody}}
11.23 +{\end{isabellebody}}
11.24 +
11.25 +\newcommand{\nJava}{\it NanoJava}
11.26 +
11.27 +%remove clutter from the toc
11.28 +\setcounter{secnumdepth}{3}
11.29 +\setcounter{tocdepth}{2}
11.30 +
11.31 +\begin{document}
11.32 +
11.33 +\title{\nJava}
11.34 +\author{David von Oheimb \\ Tobias Nipkow}
11.35 +\maketitle
11.36 +
11.37 +\begin{abstract}\noindent
11.38 + These theories define {\nJava}, a very small fragment of the programming
11.39 + language Java (with essentially just classes) derived from the one given
11.40 + in \cite{NipkowOP00}.
11.41 + For {\nJava}, an operational semantics is given as well as a Hoare logic,
11.42 + which is proved both sound and (relatively) complete. The Hoare logic
11.43 + implements a new approach for handling auxiliary variables.
11.44 + A more complex Hoare logic covering a much larger subset of Java is described
11.45 + in \cite{DvO-CPE01}.\\
11.46 +See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
11.47 +\end{abstract}
11.48 +
11.49 +\tableofcontents
11.50 +\parindent 0pt \parskip 0.5ex
11.51 +
11.52 +\newpage
11.53 +\input{session}
11.54 +
11.55 +\newpage
11.56 +\nocite{*}
11.57 +\bibliographystyle{abbrv}
11.58 +\bibliography{root}
11.59 +
11.60 +\end{document}