Towards Certified Slicing.
Daniel Wasserrab · 2008
Slicing is a widely-used technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correctness of slicing, which should ideally be proven independent of concrete programming languages and with the help of well-known verifying techniques such as proof assistants. As a first step in this direction, this contribution presents a framework for dynamic [2] and static intraprocedural slicing [1] based on control flow and program dependence graphs. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and well-formedness properties. We provide two instantiations to show the validity of the framework: a simple While language and the sophisticated object-oriented byte code language from Jinja [3]. 0.1 Auxiliary lemmas theory AuxLemmas imports Main begin abbreviation arbitrary = = undefined Lemmas about left- and rightmost elements in lists lemma leftmost-element-property: assumes ∃ x ∈ set xs. P x obtains zs x ′ ys where xs = zs@x ′ #ys and P x ′ and ∀ z ∈ set zs. ¬ P z proof(atomize-elim) from 〈 ∃ x ∈ set xs. P x 〉 show ∃ zs x ′ ys. xs = zs @ x ′ # ys ∧ P x ′ ∧ ( ∀ z∈set zs. ¬ P z) proof(induct xs) case Nil thus?case by simp next case (Cons x ′ xs ′) note IH = 〈 ∃ a∈set xs ′. P a = ⇒ ∃ zs x ′ ys. xs ′ =