# HG changeset patch # User schirmer # Date 1026306422 -7200 # Node ID f75dfc606ac76766d04d6c73d306cf0e1dc7e95a # Parent 1bd21b082466d519fd21839311244c9fe566a1b9 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet). diff -r 1bd21b082466 -r f75dfc606ac7 src/HOL/Bali/AxCompl.thy --- a/src/HOL/Bali/AxCompl.thy Wed Jul 10 14:51:18 2002 +0200 +++ b/src/HOL/Bali/AxCompl.thy Wed Jul 10 15:07:02 2002 +0200 @@ -467,6 +467,43 @@ apply (auto dest: eval_type_sound) done +(* FIXME To TypeSafe *) +lemma wf_eval_Fin: + assumes wf: "wf_prog G" and + wt_c1: "\prg = G, cls = C, lcl = L\\In1r c1\Inl (PrimT Void)" and + conf_s0: "Norm s0\\(G, L)" and + eval_c1: "G\Norm s0 \c1\ (x1,s1)" and + eval_c2: "G\Norm s1 \c2\ s2" and + s3: "s3=abupd (abrupt_if (x1\None) x1) s2" + shows "G\Norm s0 \c1 Finally c2\ 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: +"\wf_prog G; G,A\{=:n} In1r stmt1\ {G\}; G,A\{=:n} In1r stmt2\ {G\}\ + \ G,(A\state triple set)\{=:n} In1r (stmt1 Finally stmt2)\ {G\}" +apply (tactic "wt_conf_prepare_tac 1") +apply (rule_tac Q = " (\Y' s' s. normal s \ G\s \stmt1\ s' \ s\\(G, L)) +\. G\init\n" in ax_derivs.Fin) +apply (tactic "forw_hyp_tac 1") +apply (tactic "clarsimp_tac eval_css 1") +apply (rule allI) +apply (tactic "clarsimp_tac eval_css 1") +apply (tactic "forw_hyp_tac 1") +apply (tactic {* pair_tac "sb" 1 *}) +apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1") +apply (rule wf_eval_Fin) +apply auto +done + text {* For @{text MGFn_lemma} we need the wellformedness of the program to switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call}, @{text MGFn_FVar}*} @@ -483,14 +520,15 @@ apply (induct_tac "t") apply (induct_tac "a") apply fast+ -apply (rule var_expr_stmt.induct) -(* 28 subgoals *) -prefer 14 apply fast (* Methd *) -prefer 13 apply (erule (3) MGFn_Call) +apply (rule var_expr_stmt.induct) +(* 34 subgoals *) +prefer 17 apply fast (* Methd *) +prefer 16 apply (erule (3) MGFn_Call) prefer 2 apply (drule MGFn_Init,erule (2) MGFn_FVar) apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *) -apply (erule_tac [23] MGFn_Init) -prefer 18 apply (erule (1) MGFn_Loop) +apply (erule_tac [29] MGFn_Init) +prefer 23 apply (erule (1) MGFn_Loop) +prefer 26 apply (erule (2) MGFn_Fin) apply (tactic "ALLGOALS compl_prepare_tac") apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1") @@ -499,6 +537,8 @@ apply (erule MGFnD [THEN ax_NormalD]) apply (tactic "forw_hyp_eval_Force_tac 1") +apply (rule ax_derivs.InstInitV) + apply (rule ax_derivs.NewC) apply (erule MGFn_InitD [THEN conseq2]) apply (tactic "eval_Force_tac 1") @@ -516,6 +556,12 @@ apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1") apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1") +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 (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") @@ -541,6 +587,10 @@ apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *}) apply (erule (1) eval.Body) +apply (rule ax_derivs.InstInitE) + +apply (rule ax_derivs.Callee) + apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1") apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1") @@ -576,14 +626,7 @@ apply (tactic "clarsimp_tac eval_css 1") apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext]) -apply (rule_tac Q = " (\Y' s' s. normal s \ G\s \stmt1\ s') \. G\init\n" in ax_derivs.Fin) -apply (tactic "forw_hyp_eval_Force_tac 1") -apply (rule allI) -apply (tactic "forw_hyp_tac 1") -apply (tactic {* pair_tac "sb" 1 *}) -apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1") -apply (drule (1) eval.Fin) -apply clarsimp +apply (rule ax_derivs.FinA) apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1") diff -r 1bd21b082466 -r f75dfc606ac7 src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Wed Jul 10 14:51:18 2002 +0200 +++ b/src/HOL/Bali/AxSem.thy Wed Jul 10 15:07:02 2002 +0200 @@ -536,6 +536,16 @@ Lit: "G,A\{Normal (P\Val v)} Lit v-\ {P}" + UnOp: "\G,A\{Normal P} e-\ {\Val:v:. Q\Val (eval_unop unop v)}\ + \ + G,A\{Normal P} UnOp unop e-\ {Q}" + + BinOp: + "\G,A\{Normal P} e1-\ {Q}; + \v1. G,A\{Q\Val v1} e2-\ {\Val:v2:. R\Val (eval_binop binop v1 v2)}\ + \ + G,A\{Normal P} BinOp binop e1 e2-\ {R}" + Super:" G,A\{Normal (\s.. P\Val (val_this s))} Super-\ {P}" Acc: "\G,A\{Normal P} va=\ {\Var:(v,f):. Q\Val v}\ \ @@ -583,7 +593,7 @@ Expr: "\G,A\{Normal P} e-\ {Q\\}\ \ G,A\{Normal P} .Expr e. {Q}" - Lab: "\G,A\{Normal P} .c. {abupd (absorb (Break l)) .; Q}\ \ + Lab: "\G,A\{Normal P} .c. {abupd (absorb l) .; Q}\ \ G,A\{Normal P} .l\ c. {Q}" Comp: "\G,A\{Normal P} .c1. {Q}; @@ -627,6 +637,14 @@ .init c. {set_lvars l .; R}\ \ G,A\{Normal (P \. Not \ initd C)} .Init C. {R}" +-- {* Some dummy rules for the intermediate terms @{text Callee}, +@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep +semantics. +*} + InstInitV: " G,A\{Normal P} InsInitV c v=\ {Q}" + InstInitE: " G,A\{Normal P} InsInitE c e-\ {Q}" + Callee: " G,A\{Normal P} Callee l e-\ {Q}" + FinA: " G,A\{Normal P} .FinA a c. {Q}" axioms (** these terms are the same as above, but with generalized typing **) polymorphic_conseq: "\Y s Z . P Y s Z \ (\P' Q'. G,A\{P'} t\ {Q'} \ (\Y' s'. @@ -667,9 +685,9 @@ apply (fast intro: ax_derivs.asm) (*apply (fast intro: ax_derivs.cut) *) apply (fast intro: ax_derivs.weaken) -apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) -(* 31 subgoals *) -prefer 16 (* Methd *) +apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) +(* 37 subgoals *) +prefer 18 (* Methd *) apply (rule ax_derivs.Methd, drule spec, erule mp, fast) apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) THEN_ALL_NEW Blast_tac) *}) @@ -696,7 +714,7 @@ lemma weaken: "G,(A::'a triple set)|\(ts'::'a triple set) \ !ts. ts \ ts' \ G,A|\ts" apply (erule ax_derivs.induct) -(*36 subgoals*) +(*42 subgoals*) apply (tactic "ALLGOALS strip_tac") apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"), etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*}) @@ -708,7 +726,7 @@ (*apply (blast intro: ax_derivs.cut) *) apply (fast intro: ax_derivs.weaken) apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *)) -(*31 subgoals*) +(*37 subgoals*) apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) THEN_ALL_NEW Fast_tac) *}) (*1 subgoal*) diff -r 1bd21b082466 -r f75dfc606ac7 src/HOL/Bali/AxSound.thy --- a/src/HOL/Bali/AxSound.thy Wed Jul 10 14:51:18 2002 +0200 +++ b/src/HOL/Bali/AxSound.thy Wed Jul 10 15:07:02 2002 +0200 @@ -313,17 +313,18 @@ "\a vs D l. (P' a vs D l \ P a vs D l) \ \a vs D l. P a vs D l" by fast + lemmas sound_lemmas = Init_sound Loop_sound Methd_sound lemma ax_sound2: "wf_prog G \ G,A|\ts \ G,A|\\ts" apply (erule ax_derivs.induct) -prefer 20 (* Call *) +prefer 22 (* Call *) apply (erule (1) Call_sound) apply simp apply force apply force apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *}) -apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac") +apply(tactic "COND (has_fewer_prems(30+9)) (ALLGOALS sound_prepare_tac) no_tac") (*empty*) apply fast (* insert *) @@ -336,7 +337,13 @@ apply (simp (no_asm_use) add: type_ok_def,fast)(* hazard *) apply force (* Abrupt *) -(* 25 subgoals *) +prefer 28 apply (simp add: evaln_InsInitV) +prefer 28 apply (simp add: evaln_InsInitE) +prefer 28 apply (simp add: evaln_Callee) +prefer 28 apply (simp add: evaln_FinA) + +(* 27 subgoals *) +apply (tactic {* sound_elim_tac 1 *}) apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *) apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() delsimps [thm "all_empty"])) *}) (* Done *) @@ -347,12 +354,11 @@ apply (simp,simp,simp) apply (frule_tac [4] wt_init_comp_ty) (* for NewA*) apply (tactic "ALLGOALS sound_valid2_tac") -apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *) +apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *) apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, dtac spec], dtac conjunct2, smp_tac 1, TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *}) -apply (frule_tac [14] x = x1 in conforms_NormI) (* for Fin *) - +apply (frule_tac [15] x = x1 in conforms_NormI) (* for Fin *) (* 15 subgoals *) (* FVar *) @@ -383,6 +389,9 @@ apply (rule conjI,blast) apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def) +(* BinOp *) +apply (tactic "sound_forw_hyp_tac 1") + (* Ass *) apply (tactic "sound_forw_hyp_tac 1") apply (case_tac "aa") diff -r 1bd21b082466 -r f75dfc606ac7 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Wed Jul 10 14:51:18 2002 +0200 +++ b/src/HOL/Bali/Eval.thy Wed Jul 10 15:07:02 2002 +0200 @@ -447,6 +447,43 @@ section "evaluation judgments" +consts eval_unop :: "unop \ val \ val" +primrec +"eval_unop UPlus v = Intg (the_Intg v)" +"eval_unop UMinus v = Intg (- (the_Intg v))" +"eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented" +"eval_unop UNot v = Bool (\ the_Bool v)" + +consts eval_binop :: "binop \ val \ val \ 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))" +"eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))" +"eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))" +"eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))" + +-- "Be aware of the explicit coercion of the shift distance to nat" +"eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))" +"eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))" +"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented" + +"eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" +"eval_binop Le v1 v2 = Bool ((the_Intg v1) \ (the_Intg v2))" +"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))" +"eval_binop Ge v1 v2 = Bool ((the_Intg v2) \ (the_Intg v1))" + +"eval_binop Eq v1 v2 = Bool (v1=v2)" +"eval_binop Neq v1 v2 = Bool (v1\v2)" +"eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented" +"eval_binop And v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" +"eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented" +"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" +"eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented" +"eval_binop Or v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" + + consts eval :: "prog \ (state \ term \ vals \ state) set" halloc:: "prog \ (state \ obj_tag \ loc \ state) set" @@ -513,7 +550,6 @@ SXcpt: "\G\Norm s0 \halloc (CInst (SXcpt xn))\a\ (x,s1)\ \ G\(Some (Xcpt (Std xn)),s0) \sxalloc\ (Some (Xcpt (Loc a)),s1)" - inductive "eval G" intros (* propagation of abrupt completion *) @@ -533,7 +569,7 @@ G\Norm s0 \Expr e\ s1" Lab: "\G\Norm s0 \c \ s1\ \ - G\Norm s0 \l\ c\ abupd (absorb (Break l)) s1" + G\Norm s0 \l\ c\ abupd (absorb l) s1" (* cf. 14.2 *) Comp: "\G\Norm s0 \c1 \ s1; G\ s1 \c2 \ s2\ \ @@ -573,9 +609,12 @@ (* cf. 14.18.2 *) Fin: "\G\Norm s0 \c1\ (x1,s1); - G\Norm s1 \c2\ s2\ \ - G\Norm s0 \c1 Finally c2\ abupd (abrupt_if (x1\None) x1) s2" - + G\Norm s1 \c2\ s2; + s3=(if (\ err. x1=Some (Error err)) + then (x1,s1) + else abupd (abrupt_if (x1\None) x1) s2) \ + \ + G\Norm s0 \c1 Finally c2\ s3" (* cf. 12.4.2, 8.5 *) Init: "\the (class G C) = c; if inited C (globs s0) then s3 = Norm s0 @@ -630,8 +669,12 @@ (* cf. 15.7.1 *) Lit: "G\Norm s \Lit v-\v\ Norm s" + UnOp: "\G\Norm s0 \e-\v\ s1\ + \ G\Norm s0 \UnOp unop e-\(eval_unop unop v)\ s1" - + BinOp: "\G\Norm s0 \e1-\v1\ s1; G\s1 \e2-\v2\ s2\ + \ G\Norm s0 \BinOp binop e1 e2-\(eval_binop binop v1 v2)\ s2" + (* cf. 15.10.2 *) Super: "G\Norm s \Super-\val_this s\ Norm s" @@ -666,11 +709,14 @@ Methd: "\G\Norm s0 \body G D sig-\v\ s1\ \ G\Norm s0 \Methd D sig-\v\ s1" - + (* The local variables l are just a dummy here. The are only used by + the smallstep semantics *) (* cf. 14.15, 12.4.1 *) Body: "\G\Norm s0 \Init D\ s1; G\s1 \c\ s2\ \ - G\Norm s0 \Body D c -\the (locals (store s2) Result)\abupd (absorb Ret) s2" - + G\Norm s0 \Body D c + -\the (locals (store s2) Result)\abupd (absorb Ret) s2" + (* The local variables l are just a dummy here. The are only used by + the smallstep semantics *) (* evaluation of variables *) (* cf. 15.13.1, 15.7.2 *) @@ -704,21 +750,24 @@ G\Norm s0 \e#es\\v#vs\ s2" (* Rearrangement of premisses: -[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst), - 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If), - 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar), - 27(AVar),22(Call)] +[0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst), + 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If), + 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar), + 29(AVar),24(Call)] *) ML {* bind_thm ("eval_induct_", rearrange_prems -[0,1,2,8,4,28,29,25,15,16, - 17,18,19,3,5,23,24,21,6, - 7,11,9,13,14,12,20,10,26, - 27,22] (thm "eval.induct")) +[0,1,2,8,4,30,31,27,15,16, + 17,18,19,20,21,3,5,25,26,23,6, + 7,11,9,13,14,12,22,10,28, + 29,24] (thm "eval.induct")) *} + + lemmas eval_induct = eval_induct_ [split_format and and and and and and and and - and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and + and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and + and and s2 (* Fin *) and and s2 (* NewC *)] declare split_if [split del] split_if_asm [split del] @@ -757,6 +806,8 @@ "G\Norm s \In3 ([]) \\ vs'" "G\Norm s \In3 (e#es) \\ vs'" "G\Norm s \In1l (Lit w) \\ vs'" + "G\Norm s \In1l (UnOp unop e) \\ vs'" + "G\Norm s \In1l (BinOp binop e1 e2) \\ vs'" "G\Norm s \In2 (LVar vn) \\ vs'" "G\Norm s \In1l (Cast T e) \\ vs'" "G\Norm s \In1l (e InstOf T) \\ vs'" @@ -802,6 +853,7 @@ apply auto done + ML_setup {* fun eval_fun nam inj rhs = let @@ -827,6 +879,68 @@ declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!] +text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only +used in smallstep semantics, not in the bigstep semantics. So their is no +valid evaluation of these terms +*} + + +lemma eval_Callee: "G\Norm s\Callee l e-\v\ s' = False" +proof - + { fix s t v s' + assume eval: "G\s \t\\ (v,s')" and + normal: "normal s" and + callee: "t=In1l (Callee l e)" + then have "False" + proof (induct) + qed (auto) + } + then show ?thesis + by (cases s') fastsimp +qed + + +lemma eval_InsInitE: "G\Norm s\InsInitE c e-\v\ s' = False" +proof - + { fix s t v s' + assume eval: "G\s \t\\ (v,s')" and + normal: "normal s" and + callee: "t=In1l (InsInitE c e)" + then have "False" + proof (induct) + qed (auto) + } + then show ?thesis + by (cases s') fastsimp +qed + +lemma eval_InsInitV: "G\Norm s\InsInitV c w=\v\ s' = False" +proof - + { fix s t v s' + assume eval: "G\s \t\\ (v,s')" and + normal: "normal s" and + callee: "t=In2 (InsInitV c w)" + then have "False" + proof (induct) + qed (auto) + } + then show ?thesis + by (cases s') fastsimp +qed + +lemma eval_FinA: "G\Norm s\FinA a c\ s' = False" +proof - + { fix s t v s' + assume eval: "G\s \t\\ (v,s')" and + normal: "normal s" and + callee: "t=In1r (FinA a c)" + then have "False" + proof (induct) + qed (auto) + } + then show ?thesis + by (cases s') fastsimp +qed lemma eval_no_abrupt_lemma: "\s s'. G\s \t\\ (w,s') \ normal s' \ normal s" @@ -909,7 +1023,8 @@ apply (case_tac "s", case_tac "a = None") by (auto intro!: eval.If) -lemma MethdI: "G\s \body G C sig-\v\ s' \ G\s \Methd C sig-\v\ s'" +lemma MethdI: "G\s \body G C sig-\v\ s' + \ G\s \Methd C sig-\v\ s'" apply (case_tac "s", case_tac "a = None") by (auto intro!: eval.Methd) @@ -979,7 +1094,8 @@ *) lemma eval_Methd: - "G\s \In1l(body G C sig)\\ (w,s') \ G\s \In1l(Methd C sig)\\ (w,s')" + "G\s \In1l(body G C sig)\\ (w,s') + \ G\s \In1l(Methd C sig)\\ (w,s')" apply (case_tac "s") apply (case_tac "a") apply clarsimp+ @@ -1025,6 +1141,12 @@ lemma split_pairD: "(x,y) = p \ x = fst p & y = snd p" by auto +lemma eval_Body: "\G\Norm s0 \Init D\ s1; G\s1 \c\ s2; + res=the (locals (store s2) Result); + s3=abupd (absorb Ret) s2\ \ + G\