chapter ‹The Framework› theory BasicDefs imports AuxLemmas begin text ‹ 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')$. › section ‹Basic Definitions› 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 ‹‹distinct_fst›› definition distinct_fst :: "('a × 'b) list ⇒ bool" where "distinct_fst ≡ distinct ∘ 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 ‹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 ‹transfer› and ‹pred› in locale ‹CFG›.›