(*<*)
theory ex09
imports Main "~~/src/HOL/IMP/Vars" "~~/src/HOL/IMP/Small_Step"
begin
(*>*)
text {* \ExerciseSheet{9}{8.~12.~2015} *}
text {*
\Exercise{Available Expressions}
*}
text {*
Regard the following function @{text "AA"}, which computes the {\em
available assignments} of a command. An available assignment is a
pair of a variable and an expression such that the variable holds
the value of the expression in the current state. The function
@{text "AA c A"} computes the available assignments after executing
command @{text "c"}, assuming that @{text "A"} is the set of
available assignments for the initial state.
Note that available assignments can be used for program
optimization, by avoiding recomputation of expressions whose value
is already available in some variable.
*}
fun AA :: "com \ (vname \ aexp) set \ (vname \ aexp) set" where
"AA SKIP A = A" |
"AA (x ::= a) A = (if x \ vars a then {} else {(x, a)})
\ {(x', a'). (x', a') \ A \ x \ {x'} \ vars a'}" |
"AA (c\<^sub>1;; c\<^sub>2) A = (AA c\<^sub>2 \ AA c\<^sub>1) A" |
"AA (IF b THEN c\<^sub>1 ELSE c\<^sub>2) A = AA c\<^sub>1 A \ AA c\<^sub>2 A" |
"AA (WHILE b DO c) A = A \ AA c A"
text {*
Show that available assignment analysis is a gen/kill analysis, i.e.,
define two functions @{text "gen"} and @{text "kill"} such that
@{text [display] "AA c A = (A \ gen c) - kill c."}
Note that the above characterization differs from the one that you
have seen on the slides, which is @{text "(A - kill c) \ gen c"}.
However, the same properties (monotonicity, etc.) can be derived
using either version.
*}
fun gen :: "com \ (vname \ aexp) set"
and "kill" :: "com \ (vname \ aexp) set"
(*<*)
where
"gen SKIP = {}" |
"gen (x ::= a) = (if x : vars a then {} else {(x,a)})" |
"gen (c1;; c2) = gen c2 \ (gen c1 - kill c2)" |
"gen (IF b THEN c1 ELSE c2) = gen c1 \ gen c2" |
"gen (WHILE b DO c) = {}" |
"kill SKIP = {}" |
"kill (x ::= a) = {(x',a'). x=x' & a\a' | x : vars a'}" |
"kill (c1;; c2) = (kill c1 - gen c2) \ kill c2" |
"kill (IF b THEN c1 ELSE c2) = kill c1 \ kill c2" |
"kill (WHILE b DO c) = kill c"
(*>*)
text {* *}
lemma AA_gen_kill: "AA c A = (A \ gen c) - kill c"
(*<*)
apply(induct c arbitrary:A)
apply auto
done
(*>*)
text {*
Hint: Defining @{text "gen"} and @{text "kill"} functions for
available assignments will require \emph{mutual recursion}, i.e.,
@{text "gen"} must make recursive calls to @{text "kill"}, and
@{text "kill"} must also make recursive calls to @{text "gen"}. The
\textbf{and}-syntax in the function declaration allows you to define
both functions simultaneously with mutual recursion. After the
\textbf{where} keyword, list all the equations for both functions,
separated by @{text "|"} as usual.
*}
(*<*)
lemma AA_mono: "A1 \ A2 \ AA c A1 \ AA c A2"
by(auto simp add: AA_gen_kill)
lemma AA_distr[simp]: "AA c (A1 \ A2) = AA c A1 \ AA c A2"
by(auto simp add: AA_gen_kill)
lemma AA_idemp[simp]: "AA c (AA c A) = AA c A"
by(auto simp add: AA_gen_kill)
(*>*)
text {* Now show that the analysis is sound: *}
theorem AA_sound:
"(c, s) \ s' \ \(x, a) \ AA c {}. s' x = aval a s'"
(*<*)oops(*>*)
text {* Hint: You will have to generalize the theorem for the induction to go
through. *}
(*<*)
lemma AA_sound_aux:
"(c,s) \ s' \ \ (x,a) \ A. s x = aval a s
\ \ (x,a) \ AA c A. s' x = aval a s'"
proof (induct arbitrary: A rule: big_step_induct)
case Assign then show ?case by (auto split: split_if_asm)
next
case Seq
from Seq(4)[OF Seq(2)[OF Seq(5)]] show ?case by simp
next
case WhileTrue
from WhileTrue(5)[OF WhileTrue(3)[OF WhileTrue(6)]]
show ?case by simp
qed auto
theorem AA_sound:
"(c,s) \ s' \ \ (x,a) \ AA c {}. s' x = aval a s'"
using AA_sound_aux[where A="{}"] by auto
(*>*)
(*<*)
end
(*>*)