theory Ex09_Template imports "../../Semantics/Com" "../../Semantics/Def_Ass_Exp" "../../Semantics/Vars" "../../Semantics/Util" begin subsection "Initialization-Sensitive Small Step Semantics" inductive small_step :: "(com \ state) \ (com \ state) \ bool" (infix "\" 55) where Assign: "aval a s = Some i \ (x ::= a, s) \ (SKIP, s(x := Some i))" | Semi1: "(SKIP;c,s) \ (c,s)" | Semi2: "(c\<^isub>1,s) \ (c\<^isub>1',s') \ (c\<^isub>1;c\<^isub>2,s) \ (c\<^isub>1';c\<^isub>2,s')" | IfTrue: "bval b s = Some True \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \ (c\<^isub>1,s)" | IfFalse: "bval b s = Some False \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \ (c\<^isub>2,s)" | While: "(WHILE b DO c,s) \ (IF b THEN c; WHILE b DO c ELSE SKIP,s)" lemmas small_step_induct = small_step.induct[split_format(complete)] inductive small_steps :: "com * state \ com * state \ bool" (infix "\*" 55) where refl: "cs \* cs" | step: "cs \ cs' \ cs' \* cs'' \ cs \* cs''" lemmas small_steps_induct = small_steps.induct[split_format(complete)] subsection "Definite Assignment Analysis" fun AA :: "com \ name set" where "AA c = {}" (* provide a suitable definition *) fun D :: "name set \ com \ bool" where "D A c = True" (* provide a suitable definition *) subsection "Soundness wrt Small Steps" theorem progress: "D (dom s) c \ c \ SKIP \ \ cs'. (c,s) \ cs'" oops lemma D_incr: "(c,s) \ (c',s') \ dom s \ AA c \ dom s' \ AA c'" oops lemma D_mono: "A \ A' \ D A c \ D A' c" oops theorem D_preservation: "(c,s) \ (c',s') \ D (dom s) c \ D (dom s') c'" oops theorem D_sound: "(c,s) \* (c',s') \ D (dom s) c \ c' \ SKIP \ \cs''. (c',s') \ cs''" oops end