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