Added conditional and (&&) and or (||).
--- a/src/HOL/Bali/AxCompl.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy Tue Jul 16 20:25:21 2002 +0200
@@ -467,24 +467,6 @@
apply (auto dest: eval_type_sound)
done
-(* FIXME To TypeSafe *)
-lemma wf_eval_Fin:
- assumes wf: "wf_prog G" and
- wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
- conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
- eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
- eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
- s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
- shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
-proof -
- from eval_c1 wt_c1 wf conf_s0
- have "error_free (x1,s1)"
- by (auto dest: eval_type_sound)
- with eval_c1 eval_c2 s3
- show ?thesis
- by - (rule eval.Fin, auto simp add: error_free_def)
-qed
-
text {* For @{text MGFn_Fin} we need the wellformedness of the program to
switch from the evaln-semantics to the eval-semantics *}
lemma MGFn_Fin:
@@ -559,8 +541,24 @@
apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1")
apply (rule ax_derivs.BinOp)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (tactic "forw_hyp_eval_Force_tac 1")
+apply (erule MGFnD [THEN ax_NormalD])
+
+apply (rule allI)
+apply (case_tac "need_second_arg binop v1")
+apply simp
+apply (tactic "forw_hyp_eval_Force_tac 1")
+
+apply simp
+apply (rule ax_Normal_cases)
+apply (rule ax_derivs.Skip [THEN conseq1])
+apply clarsimp
+
+apply (rule eval_BinOp_arg2_indepI)
+apply simp
+apply simp
+
+apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
+apply (tactic "eval_Force_tac 1")
apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
--- a/src/HOL/Bali/AxSem.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/AxSem.thy Tue Jul 16 20:25:21 2002 +0200
@@ -483,7 +483,6 @@
claset_ref () := claset () delSWrapper "split_all_tac"
*}
-
inductive "ax_derivs G" intros
empty: " G,A|\<turnstile>{}"
@@ -542,7 +541,9 @@
BinOp:
"\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
- \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} e2-\<succ> {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
+ \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1}
+ (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
+ {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
\<Longrightarrow>
G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}"
--- a/src/HOL/Bali/AxSound.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/AxSound.thy Tue Jul 16 20:25:21 2002 +0200
@@ -391,6 +391,9 @@
(* BinOp *)
apply (tactic "sound_forw_hyp_tac 1")
+apply (case_tac "need_second_arg binop v1")
+apply fastsimp
+apply simp
(* Ass *)
apply (tactic "sound_forw_hyp_tac 1")
--- a/src/HOL/Bali/Eval.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Eval.thy Tue Jul 16 20:25:21 2002 +0200
@@ -455,8 +455,6 @@
"eval_unop UNot v = Bool (\<not> the_Bool v)"
consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
-
-
primrec
"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
"eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
@@ -482,7 +480,25 @@
"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
"eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
"eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+"eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
+"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and> \<not> the_Bool v1) \<or>
+ (binop=CondOr \<and> the_Bool v1))"
+text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
+ if the value isn't already determined by the first argument*}
+
+lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b"
+by (simp add: need_second_arg_def)
+
+lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)"
+by (simp add: need_second_arg_def)
+
+lemma need_second_arg_strict[simp]:
+ "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
+by (cases binop)
+ (simp_all add: need_second_arg_def)
consts
eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set"
@@ -550,6 +566,11 @@
SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
+text {*
+\par
+*} (* dummy text command to break paragraph for latex;
+ large paragraphs exhaust memory of debian pdflatex *)
+
inductive "eval G" intros
(* propagation of abrupt completion *)
@@ -671,8 +692,11 @@
UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
-
- BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<rightarrow> s2\<rbrakk>
+
+ BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1;
+ G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
+ \<succ>\<rightarrow> (In1 v2,s2)
+ \<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
(* cf. 15.10.2 *)
@@ -764,6 +788,10 @@
*}
+text {*
+\par
+*} (* dummy text command to break paragraph for latex;
+ large paragraphs exhaust memory of debian pdflatex *)
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and
@@ -1104,6 +1132,31 @@
apply force
done
+lemma eval_binop_arg2_indep:
+"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
+by (cases binop)
+ (simp_all add: need_second_arg_def)
+
+
+lemma eval_BinOp_arg2_indepI:
+ assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
+ no_need: "\<not> need_second_arg binop v1"
+ shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
+ (is "?EvalBinOp v2")
+proof -
+ from eval_e1
+ have "?EvalBinOp Unit"
+ by (rule eval.BinOp)
+ (simp add: no_need)
+ moreover
+ from no_need
+ have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
+ by (simp add: eval_binop_arg2_indep)
+ ultimately
+ show ?thesis
+ by simp
+qed
+
section "single valued"
--- a/src/HOL/Bali/Evaln.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy Tue Jul 16 20:25:21 2002 +0200
@@ -106,7 +106,9 @@
UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
- BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n\<rightarrow> s2\<rbrakk>
+ BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1;
+ G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
+ \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
@@ -388,6 +390,21 @@
apply auto
done
+(* ##### FIXME: To WellType *)
+lemma wt_elim_BinOp:
+ "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
+ \<And>T1 T2 T3.
+ \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
+ E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
+ T = Inl (PrimT (binop_type binop))\<rbrakk>
+ \<Longrightarrow> P\<rbrakk>
+\<Longrightarrow> P"
+apply (erule wt_elim_cases)
+apply (cases b)
+apply auto
+done
+
+section {* evaln implies eval *}
lemma evaln_eval:
assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
@@ -507,8 +524,8 @@
by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
next
case BinOp
- with wf show ?case
- by - (erule wt_elim_cases, blast intro!: eval.BinOp dest: eval_type_sound)
+ with wf show ?case
+ by - (erule wt_elim_BinOp, blast intro!: eval.BinOp dest: eval_type_sound)
next
case Super
show ?case by (rule eval.Super)
@@ -1085,6 +1102,7 @@
show ?thesis .
qed
+section {* eval implies evaln *}
lemma eval_evaln:
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
@@ -1446,8 +1464,9 @@
case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
with wf obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
+ "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+ else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"
+ by (blast elim!: wt_elim_BinOp dest: eval_type_sound)
hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
\<rightarrow> s2"
by (blast intro!: evaln.BinOp dest: evaln_max2)
--- a/src/HOL/Bali/Term.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Term.thy Tue Jul 16 20:25:21 2002 +0200
@@ -60,26 +60,26 @@
-types locals = "(lname, val) table" (* local variables *)
+types locals = "(lname, val) table" --{* local variables *}
datatype jump
- = Break label (* break *)
- | Cont label (* continue *)
- | Ret (* return from method *)
+ = Break label --{* break *}
+ | Cont label --{* continue *}
+ | Ret --{* return from method *}
-datatype xcpt (* exception *)
- = Loc loc (* location of allocated execption object *)
- | Std xname (* intermediate standard exception, see Eval.thy *)
+datatype xcpt --{* exception *}
+ = Loc loc --{* location of allocated execption object *}
+ | Std xname --{* intermediate standard exception, see Eval.thy *}
datatype error
- = AccessViolation (* Access to a member that isn't permitted *)
+ = AccessViolation --{* Access to a member that isn't permitted *}
-datatype abrupt (* abrupt completion *)
- = Xcpt xcpt (* exception *)
- | Jump jump (* break, continue, return *)
- | Error error (* runtime errors, we wan't to detect and proof absent
- in welltyped programms *)
+datatype abrupt --{* abrupt completion *}
+ = Xcpt xcpt --{* exception *}
+ | Jump jump --{* break, continue, return *}
+ | Error error -- {* runtime errors, we wan't to detect and proof absent
+ in welltyped programms *}
types
abopt = "abrupt option"
@@ -92,93 +92,132 @@
translations
"locals" <= (type) "(lname, val) table"
-datatype inv_mode (* invocation mode for method calls *)
- = Static (* static *)
- | SuperM (* super *)
- | IntVir (* interface or virtual *)
+datatype inv_mode --{* invocation mode for method calls *}
+ = Static --{* static *}
+ | SuperM --{* super *}
+ | IntVir --{* interface or virtual *}
-record sig = (* signature of a method, cf. 8.4.2 *)
- name ::"mname" (* acutally belongs to Decl.thy *)
+record sig = --{* signature of a method, cf. 8.4.2 *}
+ name ::"mname" --{* acutally belongs to Decl.thy *}
parTs::"ty list"
translations
"sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
"sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
--- "function codes for unary operations"
-datatype unop = UPlus
- | UMinus
- | UBitNot
- | UNot
+--{* function codes for unary operations *}
+datatype unop = UPlus -- {*{\tt +} unary plus*}
+ | UMinus -- {*{\tt -} unary minus*}
+ | UBitNot -- {*{\tt ~} bitwise NOT*}
+ | UNot -- {*{\tt !} logical complement*}
--- "function codes for binary operations"
-datatype binop = Mul
- | Div
- | Mod
- | Plus
- | Minus
- | LShift
- | RShift
- | RShiftU
- | Less
- | Le
- | Greater
- | Ge
- | Eq
- | Neq
- | BitAnd
- | And
- | BitXor
- | Xor
- | BitOr
- | Or
+--{* function codes for binary operations *}
+datatype binop = Mul -- {*{\tt * } multiplication*}
+ | Div -- {*{\tt /} division*}
+ | Mod -- {*{\tt \%} remainder*}
+ | Plus -- {*{\tt +} addition*}
+ | Minus -- {*{\tt -} subtraction*}
+ | LShift -- {*{\tt <<} left shift*}
+ | RShift -- {*{\tt >>} signed right shift*}
+ | RShiftU -- {*{\tt >>>} unsigned right shift*}
+ | Less -- {*{\tt <} less than*}
+ | Le -- {*{\tt <=} less than or equal*}
+ | Greater -- {*{\tt >} greater than*}
+ | Ge -- {*{\tt >=} greater than or equal*}
+ | Eq -- {*{\tt ==} equal*}
+ | Neq -- {*{\tt !=} not equal*}
+ | BitAnd -- {*{\tt \&} bitwise AND*}
+ | And -- {*{\tt \&} boolean AND*}
+ | BitXor -- {*{\texttt \^} bitwise Xor*}
+ | Xor -- {*{\texttt \^} boolean Xor*}
+ | BitOr -- {*{\tt |} bitwise Or*}
+ | Or -- {*{\tt |} boolean Or*}
+ | CondAnd -- {*{\tt \&\&} conditional And*}
+ | CondOr -- {*{\tt ||} conditional Or *}
+text{* The boolean operators {\tt \&} and {\tt |} strictly evaluate both
+of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only
+evaluate the second argument if the value of the whole expression isn't
+allready determined by the first argument.
+e.g.: {\tt false \&\& e} e is not evaluated;
+ {\tt true || e} e is not evaluated;
+*}
datatype var
- = LVar lname(* local variable (incl. parameters) *)
- | FVar qtname qtname bool expr vname
- (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
- | AVar expr expr (* array component *) ("_.[_]"[90,10 ]90)
- | InsInitV stmt var (* insertion of initialization before
- evaluation of var (for smallstep sem.) *)
+ = LVar lname --{* local variable (incl. parameters) *}
+ | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
+ --{* class field *}
+ --{* @{term "{accC,statDeclC,stat}e..fn"} *}
+ --{* @{text accC}: accessing class (static class were *}
+ --{* the code is declared. Annotation only needed for *}
+ --{* evaluation to check accessibility) *}
+ --{* @{text statDeclC}: static declaration class of field*}
+ --{* @{text stat}: static or instance field?*}
+ --{* @{text e}: reference to object*}
+ --{* @{text fn}: field name*}
+ | AVar expr expr ("_.[_]"[90,10 ]90)
+ --{* array component *}
+ --{* @{term "e1.[e2]"}: e1 array reference; e2 index *}
+ | InsInitV stmt var
+ --{* insertion of initialization before evaluation *}
+ --{* of var (technical term for smallstep semantics.)*}
and expr
- = NewC qtname (* class instance creation *)
- | NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85)
- | Cast ty expr (* type cast *)
- | Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85)
- | Lit val (* literal value, references not allowed *)
- | UnOp unop expr (* unary operation *)
- | BinOp binop expr expr (* binary operation *)
+ = NewC qtname --{* class instance creation *}
+ | NewA ty expr ("New _[_]"[99,10 ]85)
+ --{* array creation *}
+ | Cast ty expr --{* type cast *}
+ | Inst expr ref_ty ("_ InstOf _"[85,99] 85)
+ --{* instanceof *}
+ | Lit val --{* literal value, references not allowed *}
+ | UnOp unop expr --{* unary operation *}
+ | BinOp binop expr expr --{* binary operation *}
- | Super (* special Super keyword *)
- | Acc var (* variable access *)
- | Ass var expr (* variable assign *) ("_:=_" [90,85 ]85)
- | Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80)
- | Call qtname ref_ty inv_mode expr mname "(ty list)"
- "(expr list)" (* method call *)
- ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
- | Methd qtname sig (* (folded) method (see below) *)
- | Body qtname stmt (* (unfolded) method body *)
- | InsInitE stmt expr (* insertion of initialization before
- evaluation of expr (for smallstep sem.) *)
- | Callee locals expr (* save Callers locals in Callee-Frame
- (for smallstep semantics) *)
+ | Super --{* special Super keyword *}
+ | Acc var --{* variable access *}
+ | Ass var expr ("_:=_" [90,85 ]85)
+ --{* variable assign *}
+ | Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}
+ | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"
+ ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
+ --{* method call *}
+ --{* @{term "{accC,statT,mode}e\<cdot>mn({pTs}args)"} " *}
+ --{* @{text accC}: accessing class (static class were *}
+ --{* the call code is declared. Annotation only needed for*}
+ --{* evaluation to check accessibility) *}
+ --{* @{text statT}: static declaration class/interface of *}
+ --{* method *}
+ --{* @{text mode}: invocation mode *}
+ --{* @{text e}: reference to object*}
+ --{* @{text mn}: field name*}
+ --{* @{text pTs}: types of parameters *}
+ --{* @{text args}: the actual parameters/arguments *}
+ | Methd qtname sig --{* (folded) method (see below) *}
+ | Body qtname stmt --{* (unfolded) method body *}
+ | InsInitE stmt expr
+ --{* insertion of initialization before *}
+ --{* evaluation of expr (technical term for smallstep sem.) *}
+ | Callee locals expr --{* save callers locals in callee-Frame *}
+ --{* (technical term for smallstep semantics) *}
and stmt
- = Skip (* empty statement *)
- | Expr expr (* expression statement *)
- | Lab jump stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66)
- (* handles break *)
+ = Skip --{* empty statement *}
+ | Expr expr --{* expression statement *}
+ | Lab jump stmt ("_\<bullet> _" [ 99,66]66)
+ --{* labeled statement; handles break *}
| Comp stmt stmt ("_;; _" [ 66,65]65)
- | If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
- | Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
- | Do jump (* break, continue, return *)
+ | If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
+ | Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
+ | Do jump --{* break, continue, return *}
| Throw expr
- | TryC stmt
- qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70)
+ | TryC stmt qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70)
+ --{* @{term "Try c1 Catch(C vn) c2"} *}
+ --{* @{text c1}: block were exception may be thrown *}
+ --{* @{text C}: execption class to catch *}
+ --{* @{text vn}: local name for exception used in @{text c2}*}
+ --{* @{text c2}: block to execute when exception is cateched*}
| Fin stmt stmt ("_ Finally _" [ 79,79]70)
- | FinA abopt stmt (* Save abruption of first statement
- (for smallstep sem.) *)
- | Init qtname (* class initialization *)
+ | FinA abopt stmt --{* Save abruption of first statement *}
+ --{* technical term for smallstep sem.) *}
+ | Init qtname --{* class initialization *}
text {*
@@ -220,7 +259,7 @@
"!!v" == "Acc (LVar (EName (VNam v)))"
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)"
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret"
- (* Res := e;; Do Ret *)
+ --{* \tt Res := e;; Do Ret *}
"StatRef rt" == "Cast (RefT rt) (Lit Null)"
constdefs
--- a/src/HOL/Bali/Trans.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Trans.thy Tue Jul 16 20:25:21 2002 +0200
@@ -11,7 +11,6 @@
theory Trans = Evaln:
-
constdefs groundVar:: "var \<Rightarrow> bool"
"groundVar v \<equiv> (case v of
LVar ln \<Rightarrow> True
@@ -162,13 +161,19 @@
BinOpE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
-BinOpE2: "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
+BinOpE2: "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
\<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
+BinOpTerm: "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
BinOp: "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
-
+(* Maybe its more convenient to add: need_second_arg as precondition to BinOp
+ to make the choice between BinOpTerm and BinOp deterministic *)
+
Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
--- a/src/HOL/Bali/TypeSafe.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Tue Jul 16 20:25:21 2002 +0200
@@ -854,6 +854,10 @@
subsection "accessibility"
+text {*
+\par
+*} (* dummy text command to break paragraph for latex;
+ large paragraphs exhaust memory of debian pdflatex *)
(* #### stat raus und gleich is_static f schreiben *)
theorem dynamic_field_access_ok:
@@ -1707,7 +1711,9 @@
next
case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
- have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" .
+ have hyp_e2: "PROP ?TypeSafe s1 s2
+ (if need_second_arg binop v1 then In1l e2 else In1r Skip)
+ (In1 v2)" .
have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
then obtain e1T e2T where
@@ -1716,20 +1722,22 @@
wt_binop: "wt_binop G binop e1T e2T" and
T: "T=Inl (PrimT (binop_type binop))"
by (auto elim!: wt_elim_cases)
+ have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
+ by simp
from conf_s0 wt_e1
obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
error_free_s1: "error_free s1"
by (auto dest!: hyp_e1)
- from conf_s1 wt_e2 error_free_s1
+ from conf_s1 wt_e2 wt_Skip error_free_s1
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
- wt_v2: "normal s2 \<longrightarrow> G,store s2\<turnstile>v2\<Colon>\<preceq>e2T" and
error_free_s2: "error_free s2"
- by (auto dest!: hyp_e2)
- from wt_v1 wt_v2 wt_binop T
+ by (cases "need_second_arg binop v1")
+ (auto dest!: hyp_e2 )
+ from wt_binop T
have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
by (cases binop) auto
- with conf_s2 error_free_s2
+ with conf_s2 conf_s1 error_free_s2 error_free_s1
show "s2\<Colon>\<preceq>(G, L) \<and>
(normal s2 \<longrightarrow>
G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
@@ -2364,6 +2372,12 @@
qed
then show ?thesis .
qed
+
+text {*
+
+
+*} (* dummy text command to break paragraph for latex;
+ large paragraphs exhaust memory of debian pdflatex *)
corollary eval_ts:
"\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T\<rbrakk>
@@ -2395,4 +2409,22 @@
apply (drule (3) eval_type_sound)
apply clarsimp
done
+
+lemma wf_eval_Fin:
+ assumes wf: "wf_prog G" and
+ wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
+ conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
+ eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
+ eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
+ s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
+ shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
+proof -
+ from eval_c1 wt_c1 wf conf_s0
+ have "error_free (x1,s1)"
+ by (auto dest: eval_type_sound)
+ with eval_c1 eval_c2 s3
+ show ?thesis
+ by - (rule eval.Fin, auto simp add: error_free_def)
+qed
+
end
--- a/src/HOL/Bali/WellType.thy Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/WellType.thy Tue Jul 16 20:25:21 2002 +0200
@@ -216,6 +216,8 @@
"binop_type Xor = Boolean"
"binop_type BitOr = Integer"
"binop_type Or = Boolean"
+"binop_type CondAnd = Boolean"
+"binop_type CondOr = Boolean"
consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
primrec
@@ -239,8 +241,10 @@
"wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
"wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
"wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-
+
types tys = "ty + ty list"
translations
"tys" <= (type) "ty + ty list"
--- a/src/HOL/Bali/document/root.tex Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/document/root.tex Tue Jul 16 20:25:21 2002 +0200
@@ -152,6 +152,9 @@
for the maximal recursive depth. The semantics is not altered. The annotation
is needed for the soundness proof of the axiomatic semantics.
+\item[Trans]
+A smallstep operational semantics for JavaCard.
+
\item[AxSem]
An axiomatic semantics (Hoare logic) for JavaCard.
@@ -209,6 +212,8 @@
\chapter{Evaln}
\input{Evaln}
+\chapter{Trans}
+\input{Trans}
\chapter{AxSem}
\input{AxSem}
\chapter{AxSound}