Extending Slices of Object-Z Classes Based on Temporal Logic
Yunfu Shen · Computer Technology and Development · 2009
In this paper,program slicing is studied and present situation of program slicing is reported,then Object-Z class slicing is investigated.In order to verify Object-Z easily,slicing is must be done.The description of class is extended and the corresponding Kripke structure is presented by taking general stack of Object-Z as a case.Then the Object-Z is sliced by object-oriented program dependence graph and the abstraction of Object-Z is realized.A result about system properties by one class or many classes with inherited relations is proved.It is proved that formula on states and events preserves under origin model and abstract model.Finally,the slicing way of Object-Z class is extended.