header {* \isachapter{The Framework}
As slicing is a program analysis that can be completely based on the
information given in the CFG, we want to provide a framework which
allows us to formalize and prove properties of slicing regardless of
the actual programming language. So the starting point for the formalization
is the definition of an abstract CFG, i.e.\ without considering features
specific for certain languages. By doing so we ensure that our framework
is as generic as possible since all proofs hold for every language whose
CFG conforms to this abstract CFG.
Static Slicing analyses a CFG prior to execution. Whereas dynamic
slicing can provide better results for certain inputs (i.e.\ trace and
initial state), static slicing is more conservative but provides
results independent of inputs.
Correctness for static slicing is defined using a weak
simulation between nodes and states when traversing the original and
the sliced graph. The weak simulation property demands that if a
(node,state) tuples $(n_1,s_1)$ simulates $(n_2,s_2)$
and making an observable move in the original graph leads from
$(n_1,s_1)$ to $(n_1',s_1')$, this tuple simulates a
tuple $(n_2,s_2)$ which is the result of making an
observable move in the sliced graph beginning in $(n_2',s_2')$.
\isaheader{Basic Definitions} *}
theory BasicDefs imports AuxLemmas begin
fun fun_upds :: "('a => 'b) => 'a list => 'b list => ('a => 'b)"
where "fun_upds f [] ys = f"
| "fun_upds f xs [] = f"
| "fun_upds f (x#xs) (y#ys) = (fun_upds f xs ys)(x := y)"
notation fun_upds ("_'(_ /[:=]/ _')")
lemma fun_upds_nth:
"[|i < length xs; length xs = length ys; distinct xs|]
==> f(xs [:=] ys)(xs!i) = (ys!i)"
proof(induct xs arbitrary:ys i)
case Nil thus ?case by simp
next
case (Cons x' xs')
note IH = `!!ys i. [|i < length xs'; length xs' = length ys; distinct xs'|]
==> f(xs' [:=] ys) (xs'!i) = ys!i`
from `distinct (x'#xs')` have "distinct xs'" and "x' ∉ set xs'" by simp_all
from `length (x'#xs') = length ys` obtain y' ys' where [simp]:"ys = y'#ys'"
and "length xs' = length ys'"
by(cases ys) auto
show ?case
proof(cases i)
case 0 thus ?thesis by simp
next
case (Suc j)
with `i < length (x'#xs')` have "j < length xs'" by simp
from IH[OF this `length xs' = length ys'` `distinct xs'`]
have "f(xs' [:=] ys') (xs'!j) = ys'!j" .
with `x' ∉ set xs'` `j < length xs'`
have "f((x'#xs') [:=] ys) ((x'#xs')!(Suc j)) = ys!(Suc j)" by fastforce
with Suc show ?thesis by simp
qed
qed
lemma fun_upds_eq:
assumes "V ∈ set xs" and "length xs = length ys" and "distinct xs"
shows "f(xs [:=] ys) V = f'(xs [:=] ys) V"
proof -
from `V ∈ set xs` obtain i where "i < length xs" and "xs!i = V"
by(fastforce simp:in_set_conv_nth)
with `length xs = length ys` `distinct xs`
have "f(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
moreover
from `i < length xs` `xs!i = V` `length xs = length ys` `distinct xs`
have "f'(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
ultimately show ?thesis using `xs!i = V` by simp
qed
lemma fun_upds_notin:"x ∉ set xs ==> f(xs [:=] ys) x = f x"
by(induct xs arbitrary:ys,auto,case_tac ys,auto)
subsection {*@{text distinct_fst}*}
definition distinct_fst :: "('a × 'b) list => bool" where
"distinct_fst ≡ distinct o map fst"
lemma distinct_fst_Nil [simp]:
"distinct_fst []"
by(simp add:distinct_fst_def)
lemma distinct_fst_Cons [simp]:
"distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
by(auto simp:distinct_fst_def image_def)
lemma distinct_fst_isin_same_fst:
"[|(x,y) ∈ set xs; (x,y') ∈ set xs; distinct_fst xs|]
==> y = y'"
by(induct xs,auto simp:distinct_fst_def image_def)
subsection{* Edge kinds *}
text {* Every procedure has a unique name, e.g. in object oriented languages
@{text pname} refers to class + procedure. *}
text {* A state is a call stack of tuples, which consists of:
\begin{enumerate}
\item data information, i.e.\ a mapping from the local variables in the call
frame to their values, and
\item control flow information, e.g.\ which node called the current procedure.
\end{enumerate}
Update and predicate edges check and manipulate only the data information
of the top call stack element. Call and return edges however may use the data and
control flow information present in the top stack element to state if this edge is
traversable. The call edge additionally has a list of functions to determine what
values the parameters have in a certain call frame and control flow information for
the return. The return edge is concerned with passing the values
of the return parameter values to the underlying stack frame. See the funtions
@{text transfer} and @{text pred} in locale @{text CFG}. *}
datatype ('var,'val,'ret,'pname) edge_kind =
UpdateEdge "('var \<rightharpoonup> 'val) => ('var \<rightharpoonup> 'val)" ("\<Up>_")
| PredicateEdge "('var \<rightharpoonup> 'val) => bool" ("'(_')⇣\<surd>")
| CallEdge "('var \<rightharpoonup> 'val) × 'ret => bool" "'ret" "'pname"
"(('var \<rightharpoonup> 'val) \<rightharpoonup> 'val) list" ("_:_\<hookrightarrow>⇘_⇙_" 70)
| ReturnEdge "('var \<rightharpoonup> 'val) × 'ret => bool" "'pname"
"('var \<rightharpoonup> 'val) => ('var \<rightharpoonup> 'val) => ('var \<rightharpoonup> 'val)" ("_\<hookleftarrow>⇘_⇙_" 70)
definition intra_kind :: "('var,'val,'ret,'pname) edge_kind => bool"
where "intra_kind et ≡ (∃f. et = \<Up>f) ∨ (∃Q. et = (Q)⇣\<surd>)"
lemma edge_kind_cases [case_names Intra Call Return]:
"[|intra_kind et ==> P; !!Q r p fs. et = Q:r\<hookrightarrow>⇘p⇙fs ==> P;
!!Q p f. et = Q\<hookleftarrow>⇘p⇙f ==> P|] ==> P"
by(cases et,auto simp:intra_kind_def)
end