论文部分内容阅读
文中对程序切片进行了研究,报告了程序切片的现状,进行了Object-Z类切片方面的调查。为使Object-Z规格易于验证,对Object-Z作切片处理是必须的。以Object-Z的通用堆栈类为实例,对类的描述进行扩展,给出了相应的Kripke结构。通过面向对象程序依赖图对Object-Z进行切片,实现了Object-Z的抽象,给出了对于一个类或具有继承关系的多个类的刻划,即证明了在状态和事件上的公式在原模型与抽象模型中保持,扩展了Object-Z类切片方法。