用Z形式化描述程序切片

程序切片是一种重要技术,已广泛地应用于软件工程的各个领域,如程序理解、维护、调试、测试、复用、度量等.虽然,越来越多的研究者致力于程序切片工作,然而由于缺少形式化方面的工作导致程序切片可能存在不一致性和模糊性.本文尝试着用Z语言来形式化描述程序切片,考虑了程序切片中诸如程序依赖图和程序切片算法等常用的方面.该形式化描述不仅能帮助人们正确地理解程序切片的含义,而且还能够从比较严格的意义上明确程序切片的应用领域.

Formalizing Program Slicing Using Z

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.Recently, more and more researchers have worked with program slicing.However,the lack of formal semantic specification for it indicates the existence of potential semantic inconsistency and ambiguity in these activities.This paper represents a research effort towards the semantic formalization for program slicing technique using Z Schema Calculus.General aspects of program slicing are considered,i.e. program dependence graphs and program slicing algorithm.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.