(*<*) theory sol03 imports "~~/src/HOL/IMP/BExp" "~~/src/HOL/IMP/ASM" begin (*>*) text {* \ExerciseSheet{3}{27.~10.~2015} *} text {* \Exercise{Relational @{text "aval"}} Theory @{text AExp} defines an evaluation function @{text "aval :: aexp \ state \ val"} for arithmetic expressions. Define a corresponding evaluation relation @{text "is_aval :: aexp \ state \ val \ bool"} as an inductive predicate: *} inductive is_aval :: "aexp \ state \ val \ bool" (*<*)where "is_aval (N n) s n" | "s x = v \ is_aval (V x) s v" | "\is_aval a1 s v1; is_aval a2 s v2; v'=v1+v2\ \ is_aval (Plus a1 a2) s v'" (*>*) text {* Use the introduction rules @{text is_aval.intros} to prove this example lemma. *} lemma "is_aval (Plus (N 2) (Plus (V x) (N 3))) s (2 + (s x + 3))" (*<*) by (auto intro!: is_aval.intros) (*>*) text {* Prove that the evaluation relation @{text is_aval} agrees with the evaluation function @{text aval}. Show implications in both directions, and then prove the if-and-only-if form. *} lemma aval1: "is_aval a s v \ aval a s = v" (*<*) by (induction rule: is_aval.induct) auto (*>*) lemma aval2: "aval a s = v \ is_aval a s v" (*<*) by (induction a arbitrary: v) (auto intro: is_aval.intros) (*>*) theorem "is_aval a s v \ aval a s = v" (*<*) proof assume "is_aval a s v" thus "aval a s = v" by (rule aval1) next assume "aval a s = v" thus "is_aval a s v" by (rule aval2) qed (*>*) (*<*) (*The version without equality assumptions also works.*) inductive is_aval' :: "aexp \ state \ val \ bool" where "is_aval' (N n) s n" | "is_aval' (V x) s (s x)" | "\is_aval' a1 s v1; is_aval' a2 s v2\ \ is_aval' (Plus a1 a2) s (v1 + v2)" lemma "is_aval' (Plus (V x) (Plus (V y) (N 3))) s (s x + (s y + 3))" by (auto intro!: is_aval'.intros) theorem "is_aval' a s v \ aval a s = v" apply (rule iffI) apply (induction rule: is_aval'.induct) apply auto apply (induction a arbitrary: v) apply (auto intro: is_aval'.intros) done (*>*) text {* \Exercise{Avoiding Stack Underflow}*} text {* A \emph{stack underflow} occurs when executing an instruction on a stack containing too few values -- e.g., executing an @{text ADD} instruction on an stack of size less than two. A well-formed sequence of instructions (e.g., one generated by @{text comp}) should never cause a stack underflow. *} (* Alternative: functional solution: *) text {* In this exercise, you will define a semantics for the stack-machine that throws an exception if the program underflows the stack. *} text {* Modify the @{text "exec1"} and @{text "exec"} - functions, such that they return an option value, @{text "None"} indicating a stack-underflow. *} fun exec1 :: "instr \ state \ stack \ stack option" (*<*) where "exec1 (LOADI n) _ stk = Some (n # stk)" | "exec1 (LOAD x) s stk = Some (s(x) # stk)" | "exec1 ADD _ stk = ( if length (stk)\2 then Some ((hd2 stk + hd stk) # tl2 stk) else None)" (*>*) fun exec :: "instr list \ state \ stack \ stack option" (*<*) where "exec [] _ stk = Some stk" | "exec (i#is) s stk = (case exec1 i s stk of Some stk \ exec is s stk | None \ None)" (*>*) text {* Now adjust the proof of theorem @{text "exec_comp"} to show that programs output by the compiler never underflow the stack: *} (*<*) lemma exec_append[simp]: "exec (is1@is2) s stk = (case exec is1 s stk of Some stk \ exec is2 s stk | None \ None)" apply(induction is1 arbitrary: stk) apply (auto split: option.split) done (*>*) theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)" (*<*) apply(induction a arbitrary: stk) apply (auto) done (*>*) (*<*) (* Alternative: Relational solution *) text {* In this exercise, you will define a relational semantics for the stack-machine. The relation does not contain elements for programs causing a stack underflow. *} inductive execi1 :: "instr \ state \ stack \ stack \ bool" where "execi1 (LOADI n) s stk (n#stk)" | "execi1 (LOAD x) s stk (s x#stk)" | "execi1 (ADD) _ (v1#v2#stk) ((v1+v2)#stk)" lemma assumes "execi1 i s stk stk'" shows "ASM.exec1 i s stk = stk'" using assms by induction auto lemma assumes "ASM.exec1 i s stk = stk'" shows "execi1 i s stk stk'" nitpick oops inductive execi :: "instr list \ state \ stack \ stack \ bool" where "execi [] s stk stk" | "\ execi1 i s stk stk2; execi is s stk2 stk' \ \ execi (i#is) s stk stk'" lemma execi_appendI: assumes E1: "execi is1 s stk stk2" and E2: "execi is2 s stk2 stk'" shows "execi (is1@is2) s stk stk'" using E1 E2 by (induction) (auto intro: execi.intros) lemma execi_appendE[elim]: assumes "execi (is1@is2) s stk stk'" obtains stk2 where "execi is1 s stk stk2" and "execi is2 s stk2 stk'" using assms apply (induction is1 arbitrary: stk) apply (auto intro: execi.intros) [] apply (erule execi.cases) apply (auto intro: execi.intros) (*apply (force intro: execi.intros elim!: execi.cases)*) done lemma execi_sound: shows "execi (comp a) s stk (aval a s # stk)" apply (induction a arbitrary: stk) apply (auto intro!: execi.intros execi1.intros execi_appendI simp: add.commute) done inductive_cases [elim!]: "execi [LOADI i] s stk stk'" "execi [LOAD x] s stk stk'" "execi [ADD] s stk stk'" "execi [] s stk stk'" lemma execi_complete: assumes "execi (comp a) s stk stk'" shows "stk' = aval a s#stk" using assms apply (induction a arbitrary: s stk stk') apply (auto elim: execi1.cases) [2] apply (fastforce elim: execi1.cases) done theorem execi_correct: "execi (comp a) s stk stk' \ (stk' = aval a s # stk)" using execi_sound execi_complete by blast (*>*) text {* \Exercise{Avoiding Stack Overflow}*} text \ Now, modify the semantics such that @{term None} is returned if the stack gets longer than a fixed size @{text maxsize}. Define a function that, for a given expression, returns a suitable stack size, and show that the stack does not overflow. \ context fixes maxsize :: nat begin text \The @{text context} construct allows you to locally fix some value. Once you close the context, this value becomes a parameter of everything defined inside the context.\ text \Work with the following operation, which ensures that the stack does not overflow:\ definition push :: "val \ stack \ stack option" where "push i stk \ if length stk < maxsize then Some (i#stk) else None" fun exec'1 :: "instr \ state \ stack \ stack option" (*<*) where "exec'1 (LOADI n) _ stk = push n stk" | "exec'1 (LOAD x) s stk = push (s x) stk" | "exec'1 ADD _ stk = ( if length (stk)\2 then push ((hd2 stk + hd stk)) (tl2 stk) else None)" (*>*) fun exec' :: "instr list \ state \ stack \ stack option" (*<*) where "exec' [] _ stk = Some stk" | "exec' (i#is) s stk = (case exec'1 i s stk of Some stk \ exec' is s stk | None \ None)" (*>*) end -- \End of context\ text \Function to return the minimum required stack size for a given expression\ fun stacksize :: "aexp \ nat" (*<*) where "stacksize (N _) = 1" | "stacksize (V _) = 1" | "stacksize (Plus a1 a2) = max (stacksize a1) (stacksize a2) + 1" (*>*) (*<*) lemma exec_append'[simp]: "exec' ms (is1@is2) s stk = (case exec' ms is1 s stk of Some stk \ exec' ms is2 s stk | None \ None)" apply(induction is1 arbitrary: stk) apply (auto split: option.split) done lemma exec_comp'_aux: "stacksize a + length stk \ maxsize \ exec' maxsize (comp a) s stk = Some (aval a s # stk)" apply(induction a arbitrary: stk) apply (auto split: option.splits simp: push_def) done (*>*) text \Prove the correctness lemma: Hint: For the induction to go through, you need to generalize the lemma over the stack! \ theorem exec_comp': "stacksize a \ maxsize \ exec' maxsize (comp a) s [] = Some ([aval a s])" (*<*) using exec_comp'_aux by simp (*>*) (*<*) end (*>*)