Formal specification of program slicing

Program slicing is a well-known technique that has been used in a variety of software engineering areas, such as comprehension, understanding, maintenance, debugging, testing, reuse, metrics, etc. This paper discusses how the formal specification language Z schema calculus may be used to specify program slicing. General aspects of program slicing are considered, i.e. dependence graphs and program slicing algorithms. This formalization could help in the correct understanding of program slicing and also the correct application of a desired slicing regime in a rigorous way.