Up to index of Isabelle/HOL/Jinja
theory BVExample(* Title: Jinja/BV/BVExample.thy ID: $Id: BVExample.thy,v 1.12 2009-07-14 09:00:10 fhaftmann Exp $ Author: Gerwin Klein *) header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} theory BVExample imports "../JVM/JVMListExample" BVSpecTypeSafe BVExec Executable_Set Efficient_Nat begin text {* This theory shows type correctness of the example program in section \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by explicitly providing a welltyping. It also shows that the start state of the program conforms to the welltyping; hence type safe execution is guaranteed. *} section "Setup" lemma distinct_classes': "list_name ≠ test_name" "list_name ≠ Object" "list_name ≠ ClassCast" "list_name ≠ OutOfMemory" "list_name ≠ NullPointer" "test_name ≠ Object" "test_name ≠ OutOfMemory" "test_name ≠ ClassCast" "test_name ≠ NullPointer" "ClassCast ≠ NullPointer" "ClassCast ≠ Object" "NullPointer ≠ Object" "OutOfMemory ≠ ClassCast" "OutOfMemory ≠ NullPointer" "OutOfMemory ≠ Object" by (simp_all add: list_name_def test_name_def Object_def NullPointer_def OutOfMemory_def ClassCast_def) lemmas distinct_classes = distinct_classes' distinct_classes' [symmetric] lemma distinct_fields: "val_name ≠ next_name" "next_name ≠ val_name" by (simp_all add: val_name_def next_name_def) text {* Abbreviations for definitions we will have to use often in the proofs below: *} lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def lemmas class_defs = list_class_def test_class_def text {* These auxiliary proofs are for efficiency: class lookup, subclass relation, method and field lookup are computed only once: *} lemma class_Object [simp]: "class E Object = Some (undefined, [],[])" by (simp add: class_def system_defs E_def) lemma class_NullPointer [simp]: "class E NullPointer = Some (Object, [], [])" by (simp add: class_def system_defs E_def distinct_classes) lemma class_OutOfMemory [simp]: "class E OutOfMemory = Some (Object, [], [])" by (simp add: class_def system_defs E_def distinct_classes) lemma class_ClassCast [simp]: "class E ClassCast = Some (Object, [], [])" by (simp add: class_def system_defs E_def distinct_classes) lemma class_list [simp]: "class E list_name = Some list_class" by (simp add: class_def system_defs E_def distinct_classes) lemma class_test [simp]: "class E test_name = Some test_class" by (simp add: class_def system_defs E_def distinct_classes) lemma E_classes [simp]: "{C. is_class E C} = {list_name, test_name, NullPointer, ClassCast, OutOfMemory, Object}" by (auto simp add: is_class_def class_def system_defs E_def class_defs) text {* The subclass releation spelled out: *} lemma subcls1: "subcls1 E = {(list_name,Object), (test_name,Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}" (*<*) apply (simp add: subcls1_def2) apply (simp add: class_defs system_defs E_def class_def) (* FIXME: cannot simply expand class names, since inequality proofs on strings are too inefficient *) apply (auto simp: distinct_classes split: split_if_asm) done (*>*) text {* The subclass relation is acyclic; hence its converse is well founded: *} lemma notin_rtrancl: "(a,b) ∈ r* ==> a ≠ b ==> (!!y. (a,y) ∉ r) ==> False" by (auto elim: converse_rtranclE) lemma acyclic_subcls1_E: "acyclic (subcls1 E)" (*<*) apply (rule acyclicI) apply (simp add: subcls1) apply (auto dest!: tranclD) apply (auto elim!: notin_rtrancl simp add: distinct_classes) done (*>*) lemma wf_subcls1_E: "wf ((subcls1 E)¯)" (*<*) apply (rule finite_acyclic_wf_converse) apply (simp add: subcls1) apply (rule acyclic_subcls1_E) done (*>*) text {* Method and field lookup: *} lemma method_append [simp]: "method E list_name append_name = (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])" (*<*) apply (insert class_list) apply (unfold list_class_def) apply (fastsimp simp add: Method_def distinct_classes intro: method_def2 Methods.intros) done (*>*) lemma method_makelist [simp]: "method E test_name makelist_name = (test_name, [], Void, 3, 2, make_list_ins, [])" (*<*) apply (insert class_test) apply (unfold test_class_def) apply (fastsimp simp add: Method_def distinct_classes intro: method_def2 Methods.intros) done (*>*) lemma field_val [simp]: "field E list_name val_name = (list_name, Integer)" (*<*) apply (insert class_list) apply (unfold list_class_def) apply (fastsimp simp add: sees_field_def distinct_classes intro: field_def2 Fields.intros) done (*>*) lemma field_next [simp]: "field E list_name next_name = (list_name, Class list_name)" (*<*) apply (insert class_list) apply (unfold list_class_def) apply (fastsimp simp add: distinct_fields sees_field_def distinct_classes intro: field_def2 Fields.intros) done (*>*) lemma [simp]: "fields E Object = []" by (fastsimp intro: fields_def2 Fields.intros) lemma [simp]: "fields E NullPointer = []" by (fastsimp simp add: distinct_classes intro: fields_def2 Fields.intros) lemma [simp]: "fields E ClassCast = []" by (fastsimp simp add: distinct_classes intro: fields_def2 Fields.intros) lemma [simp]: "fields E OutOfMemory = []" by (fastsimp simp add: distinct_classes intro: fields_def2 Fields.intros) lemma [simp]: "fields E test_name = []" (*<*) apply (insert class_test) apply (unfold test_class_def) apply (fastsimp simp add: distinct_classes intro: fields_def2 Fields.intros) done (*>*) lemmas [simp] = is_class_def section "Program structure" text {* The program is structurally wellformed: *} lemma wf_struct: "wf_prog (λG C mb. True) E" (is "wf_prog ?mb E") (*<*) proof - have "distinct_fst E" by (simp add: system_defs E_def class_defs distinct_classes) moreover have "set SystemClasses ⊆ set E" by (simp add: system_defs E_def) hence "wf_syscls E" by (rule wf_syscls) moreover have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def) moreover have "wf_cdecl ?mb E NullPointerC" by (auto elim: notin_rtrancl simp add: wf_cdecl_def distinct_classes NullPointerC_def subcls1) moreover have "wf_cdecl ?mb E ClassCastC" by (auto elim: notin_rtrancl simp add: wf_cdecl_def distinct_classes ClassCastC_def subcls1) moreover have "wf_cdecl ?mb E OutOfMemoryC" by (auto elim: notin_rtrancl simp add: wf_cdecl_def distinct_classes OutOfMemoryC_def subcls1) moreover have "wf_cdecl ?mb E (list_name, list_class)" apply (auto elim!: notin_rtrancl simp add: wf_cdecl_def wf_fdecl_def list_class_def wf_mdecl_def subcls1) apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases) done moreover have "wf_cdecl ?mb E (test_name, test_class)" apply (auto elim!: notin_rtrancl simp add: wf_cdecl_def wf_fdecl_def test_class_def wf_mdecl_def subcls1) apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases) done ultimately show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def) qed (*>*) section "Welltypings" text {* We show welltypings of the methods @{term append_name} in class @{term list_name}, and @{term makelist_name} in class @{term test_name}: *} lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def (*declare app'Invoke [simp del]*) constdefs phi_append :: tym ("φa") "φa ≡ map (λ(x,y). Some (x, map OK y)) [ ( [], [Class list_name, Class list_name]), ( [Class list_name], [Class list_name, Class list_name]), ( [Class list_name], [Class list_name, Class list_name]), ( [Class list_name, Class list_name], [Class list_name, Class list_name]), ( [Class list_name, Class list_name], [Class list_name, Class list_name]), ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]), ( [Boolean, Class list_name], [Class list_name, Class list_name]), ( [Class Object], [Class list_name, Class list_name]), ( [], [Class list_name, Class list_name]), ( [Class list_name], [Class list_name, Class list_name]), ( [Class list_name, Class list_name], [Class list_name, Class list_name]), ( [], [Class list_name, Class list_name]), ( [Void], [Class list_name, Class list_name]), ( [Class list_name], [Class list_name, Class list_name]), ( [Class list_name, Class list_name], [Class list_name, Class list_name]), ( [Void], [Class list_name, Class list_name])]" text {* The next definition and three proof rules implement an algorithm to enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} transforms a goal of the form @{prop [display] "pc < n ==> P pc"} into a series of goals @{prop [display] "P 0"} @{prop [display] "P (Suc 0)"} @{text "…"} @{prop [display] "P n"} *} constdefs intervall :: "nat => nat => nat => bool" ("_ ∈ [_, _')") "x ∈ [a, b) ≡ a ≤ x ∧ x < b" lemma pc_0: "x < n ==> (x ∈ [0, n) ==> P x) ==> P x" by (simp add: intervall_def) lemma pc_next: "x ∈ [n0, n) ==> P n0 ==> (x ∈ [Suc n0, n) ==> P x) ==> P x" (*<*) apply (cases "x=n0") apply (auto simp add: intervall_def) done (*>*) lemma pc_end: "x ∈ [n,n) ==> P x" by (unfold intervall_def) arith lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK φa)" (*<*) by (auto simp add: check_types_def phi_append_def JVM_states_unfold) (*>*) lemma wt_append [simp]: "wt_method E list_name [Class list_name] Void 3 0 append_ins [(Suc 0, 2, NullPointer, 7, 0)] φa" (*<*) apply (simp add: wt_method_def wt_start_def wt_instr_def) apply (simp add: append_ins_def phi_append_def) apply clarify apply (drule sym) apply (erule_tac P="?x = ?y" in rev_mp) apply (elim pc_end pc_next pc_0) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: matches_ex_entry_def subcls1 relevant_entries_def is_relevant_entry_def sees_field_def list_class_def distinct_classes distinct_fields intro: Fields.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def sees_field_def list_class_def distinct_classes distinct_fields intro: Fields.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def subcls1) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def sees_field_def list_class_def distinct_classes distinct_fields intro: Fields.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def list_class_def distinct_classes Method_def intro: Methods.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) done (*>*) text {* Some abbreviations for readability *} abbreviation "Clist == Class list_name" abbreviation "Ctest == Class test_name" constdefs phi_makelist :: tym ("φm") "φm ≡ map (λ(x,y). Some (x, y)) [ ( [], [OK Ctest, Err , Err ]), ( [Clist], [OK Ctest, Err , Err ]), ( [], [OK Clist, Err , Err ]), ( [Clist], [OK Clist, Err , Err ]), ( [Integer, Clist], [OK Clist, Err , Err ]), ( [], [OK Clist, Err , Err ]), ( [Clist], [OK Clist, Err , Err ]), ( [], [OK Clist, OK Clist, Err ]), ( [Clist], [OK Clist, OK Clist, Err ]), ( [Integer, Clist], [OK Clist, OK Clist, Err ]), ( [], [OK Clist, OK Clist, Err ]), ( [Clist], [OK Clist, OK Clist, Err ]), ( [], [OK Clist, OK Clist, OK Clist]), ( [Clist], [OK Clist, OK Clist, OK Clist]), ( [Integer, Clist], [OK Clist, OK Clist, OK Clist]), ( [], [OK Clist, OK Clist, OK Clist]), ( [Clist], [OK Clist, OK Clist, OK Clist]), ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), ( [Void], [OK Clist, OK Clist, OK Clist]), ( [], [OK Clist, OK Clist, OK Clist]), ( [Clist], [OK Clist, OK Clist, OK Clist]), ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), ( [Void], [OK Clist, OK Clist, OK Clist])]" lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK φm)" (*<*) by (auto simp add: check_types_def phi_makelist_def JVM_states_unfold) (*>*) lemma wt_makelist [simp]: "wt_method E test_name [] Void 3 2 make_list_ins [] φm" (*<*) apply (simp add: wt_method_def) apply (unfold make_list_ins_def phi_makelist_def) apply (simp add: wt_start_def nat_number) apply (simp add: wt_instr_def) apply clarify apply (drule sym) apply (erule_tac P="?x = ?y" in rev_mp) apply (elim pc_end pc_next pc_0) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def sees_field_def list_class_def distinct_classes intro: Fields.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def sees_field_def list_class_def distinct_classes intro: Fields.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def sees_field_def list_class_def distinct_classes intro: Fields.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def list_class_def distinct_classes Method_def intro: Methods.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (simp add: relevant_entries_def is_relevant_entry_def) apply (fastsimp simp add: relevant_entries_def is_relevant_entry_def list_class_def distinct_classes Method_def intro: Methods.intros) apply (simp add: relevant_entries_def is_relevant_entry_def) done (*>*) lemma wf_md'E: "[| wf_prog wf_md P; !!C S fs ms m.[|(C,S,fs,ms) ∈ set P; m ∈ set ms|] ==> wf_md' P C m |] ==> wf_prog wf_md' P" (*<*) apply (simp add: wf_prog_def) apply auto apply (simp add: wf_cdecl_def wf_mdecl_def) apply fastsimp done (*>*) text {* The whole program is welltyped: *} constdefs Phi :: tyP ("Φ") "Φ C mn ≡ if C = test_name ∧ mn = makelist_name then φm else if C = list_name ∧ mn = append_name then φa else []" lemma wf_prog: "wf_jvm_progΦ E" (*<*) apply (unfold wf_jvm_prog_phi_def) apply (rule wf_md'E [OF wf_struct]) apply (simp add: E_def) apply clarify apply (fold E_def) apply (simp add: system_defs class_defs Phi_def) apply auto apply (simp add: distinct_classes) done (*>*) section "Conformance" text {* Execution of the program will be typesafe, because its start state conforms to the welltyping: *} lemma "E,Φ \<turnstile> start_state E test_name makelist_name \<surd>" (*<*) apply (rule BV_correct_initial) apply (rule wf_prog) apply (fastsimp simp add: test_class_def distinct_classes Method_def intro: Methods.intros) done (*>*) section "Example for code generation: inferring method types" constdefs test_kil :: "jvm_prog => cname => ty list => ty => nat => nat => ex_table => instr list => tyi' err list" "test_kil G C pTs rT mxs mxl et instr ≡ (let first = Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)); start = OK first#(replicate (size instr - 1) (OK None)) in kiljvm G mxs (1+size pTs+mxl) rT instr et start)" lemma [code]: "unstables r step ss = (UN p:{..<size ss}. if ¬stable r step ss p then {p} else {})" (*<*) apply (unfold unstables_def) apply (rule equalityI) apply (rule subsetI) apply (erule CollectE) apply (erule conjE) apply (rule UN_I) apply simp apply simp apply (rule subsetI) apply (erule UN_E) apply (case_tac "¬ stable r step ss p") apply simp+ done (*>*) definition some_elem :: "'a set => 'a" where "some_elem = (%S. SOME x. x : S)" consts_code "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)") (*<*) text {* This code setup is just a demonstration and \emph{not} sound! *} lemma False proof - have "some_elem (set [False, True]) = False" by evaluation moreover have "some_elem (set [True, False]) = True" by evaluation ultimately show False by (simp add: some_elem_def) qed (*>*) lemma [code]: "iter f step ss w = while (λ(ss, w). ¬ (is_empty w)) (λ(ss, w). let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) (ss, w)" unfolding iter_def List_Set.is_empty_def some_elem_def .. lemma JVM_sup_unfold [code]: "JVM_SemiType.sup S m n = lift2 (Opt.sup (Product.sup (Listn.sup (SemiType.sup S)) (λx y. OK (map2 (lift2 (SemiType.sup S)) x y))))" (*<*) apply (unfold JVM_SemiType.sup_def JVM_SemiType.sl_def Opt.esl_def Err.sl_def stk_esl_def loc_sl_def Product.esl_def Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def) by simp lemmas [code] = SemiType.sup_def [unfolded exec_lub_def] JVM_le_unfold (*>*) lemmas [code_ind_set] = rtrancl_refl converse_rtrancl_into_rtrancl lemma [code]: "is_refT T = (case T of NT => True | Class C => True | _ => False)" by (simp add: is_refT_def split add: ty.split) lemma [code_ind params: 1]: "P \<turnstile> C has_fields FDTs ==> map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = ⌊(D, T)⌋ ==> P \<turnstile> C sees F:T in D" by (auto simp add: sees_field_def) lemma [code_ind params: 1]: "P \<turnstile> C sees_methods Mm ==> Mm M = ⌊((Ts, T, m), D)⌋ ==> P \<turnstile> C sees M: Ts->T = m in D" by (auto simp add: Method_def) declare appi.simps [code] lemma [code]: "appi (Getfield F C, P, pc, mxs, Tr, (T#ST, LT)) = (∃Tf∈{Tf. sees_field P C F Tf C}. P \<turnstile> T ≤ Class C)" by auto lemma [code]: "appi (Putfield F C, P, pc, mxs, Tr, (T1#T2#ST, LT)) = (∃Tf∈{Tf. sees_field P C F Tf C}. P \<turnstile> T2 ≤ (Class C) ∧ P \<turnstile> T1 ≤ Tf)" by auto lemma [code]: "appi (Invoke M n, P, pc, mxs, Tr, (ST,LT)) = (n < length ST ∧ (ST!n ≠ NT --> (case ST!n of Class C => (∃(Ts, T, m, D)∈{(Ts, T, m, D). Method P C M Ts T m D}. P \<turnstile> rev (take n ST) [≤] Ts) | _ => False)))" by (fastsimp split add: ty.split_asm) declare field_def2 [code_ind] code_module BV contains test1 = "test_kil E list_name [Class list_name] Void 3 0 [(Suc 0, 2, NullPointer, 7, 0)] append_ins" test2 = "test_kil E test_name [] Void 3 2 [] make_list_ins" test3 = "φa" test4 = "φm" ML {* if BV.test1 = map BV.OK BV.test3 then () else error "wrong result" *} ML {* if BV.test2 = map BV.OK BV.test4 then () else error "wrong result" *} end