products/sources/formale Sprachen/Isabelle/HOL/NanoJava/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Corn.nix   Sprache: Isabelle

(*  Title:      HOL/NanoJava/OpSem.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "Operational Evaluation Semantics"

theory OpSem imports State begin

inductive
  exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\ _" [98,90, 65,98] 89)
  and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\_-_\ _"[98,95,99,65,98] 89)
where
  Skip: " s -Skip-n\ s"

| Comp: "[| s0 -c1-n\ s1; s1 -c2-n\ s2 |] ==>
            s0 -c1;; c2-n\<rightarrow> s2"

| Cond: "[| s0 -e\v-n\ s1; s1 -(if v\Null then c1 else c2)-n\ s2 |] ==>
            s0 -If(e) c1 Else c2-n\<rightarrow> s2"

| LoopF:" s0 = Null ==>
            s0 -While(x) c-n\<rightarrow> s0"
| LoopT:"[| s0 \ Null; s0 -c-n\ s1; s1 -While(x) c-n\ s2 |] ==>
            s0 -While(x) c-n\<rightarrow> s2"

| LAcc: " s -LAcc x\s-n\ s"

| LAss: " s -e\v-n\ s' ==>
            s -x:==e-n\<rightarrow> lupd(x\<mapsto>v) s'"

| FAcc: " s -e\Addr a-n\ s' ==>
            s -e..f\<succ>get_field s' a f-n\<rightarrow> s'"

| FAss: "[| s0 -e1\Addr a-n\ s1; s1 -e2\v-n\ s2 |] ==>
            s0 -e1..f:==e2-n\<rightarrow> upd_obj a f v s2"

| NewC: " new_Addr s = Addr a ==>
            s -new C\<succ>Addr a-n\<rightarrow> new_obj a C s"

| Cast: "[| s -e\v-n\ s';
            case v of Null => True | Addr a => obj_class s' a \C C |] ==>
            s -Cast C e\<succ>v-n\<rightarrow> s'"

| Call: "[| s0 -e1\a-n\ s1; s1 -e2\p-n\ s2;
            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n\<rightarrow> s3
     |] ==> s0 -{C}e1..m(e2)\<succ>s3<Res>-n\<rightarrow> set_locs s2 s3"

| Meth: "[| s = Addr a; D = obj_class s a; D\C C;
            init_locs D m s -Impl (D,m)-n\<rightarrow> s' |] ==>
            s -Meth (C,m)-n\<rightarrow> s'"

| Impl: " s -body Cm- n\ s' ==>
            s -Impl Cm-Suc n\<rightarrow> s'"


inductive_cases exec_elim_cases':
                                  "s -Skip -n\ t"
                                  "s -c1;; c2 -n\ t"
                                  "s -If(e) c1 Else c2-n\ t"
                                  "s -While(x) c -n\ t"
                                  "s -x:==e -n\ t"
                                  "s -e1..f:==e2 -n\ t"
inductive_cases Meth_elim_cases:  "s -Meth Cm -n\ t"
inductive_cases Impl_elim_cases:  "s -Impl Cm -n\ t"
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
inductive_cases eval_elim_cases:
                                  "s -new C \v-n\ t"
                                  "s -Cast C e \v-n\ t"
                                  "s -LAcc x \v-n\ t"
                                  "s -e..f \v-n\ t"
                                  "s -{C}e1..m(e2) \v-n\ t"

lemma exec_eval_mono [rule_format]: 
  "(s -c -n\ t \ (\m. n \ m \ s -c -m\ t)) \
   (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))"
apply (rule exec_eval.induct)
prefer 14 (* Impl *)
apply clarify
apply (rename_tac n)
apply (case_tac n)
apply (blast intro:exec_eval.intros)+
done
lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]

lemma exec_exec_max: "\s1 -c1- n1 \ t1 ; s2 -c2- n2\ t2\ \
                       s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
by (fast intro: exec_mono max.cobounded1 max.cobounded2)

lemma eval_exec_max: "\s1 -c- n1 \ t1 ; s2 -e\v- n2\ t2\ \
                       s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
by (fast intro: eval_mono exec_mono max.cobounded1 max.cobounded2)

lemma eval_eval_max: "\s1 -e1\v1- n1 \ t1 ; s2 -e2\v2- n2\ t2\ \
                       s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
by (fast intro: eval_mono max.cobounded1 max.cobounded2)

lemma eval_eval_exec_max: 
 "\s1 -e1\v1-n1\ t1; s2 -e2\v2-n2\ t2; s3 -c-n3\ t3\ \
   s1 -e1\<succ>v1-max (max n1 n2) n3\<rightarrow> t1 \<and> 
   s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
   s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
apply (drule (1) eval_eval_max, erule thin_rl)
by (fast intro: exec_mono eval_mono max.cobounded1 max.cobounded2)

lemma Impl_body_eq: "(\t. \n. Z -Impl M-n\ t) = (\t. \n. Z -body M-n\ t)"
apply (rule ext)
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
done

end

[ Verzeichnis aufwärts0.23unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]