Formal Abstraction of Program Slices for Specification and Requirement Extraction Using Object-Z

Program slicing is widely used in software engineering for code comprehension, debugging, and system migration. It enables developers to extract and analyze relevant code segments based on predefined criteria, improving software maintenance. However, traditional slicing approaches often lack structured formal representations, making it difficult to derive precise software specifications, especially in complex Java-based systems. This paper introduces an Object-Z-based formal approach to program slicing, ensuring precise abstraction and systematic derivation of software specifications and requirements. The proposed model employs a backward slicing technique, where Object-Z schemas provide mathematically sound and verifiable representations of program slices. This approach effectively handles Java-specific challenges, including dynamic method invocations, encapsulated class structures, and inter-procedural dependencies. The proposed Object-Z-based formal representation framework ensures functional correctness while facilitating software migration and re-engineering. Experimental validation on large-scale Java programs demonstrates that this method improves precision, reduces computational complexity, and enhances the efficiency of requirement extraction compared to traditional formal techniques. The findings highlight that integrating formal methods with program slicing enables automated specification derivation, thereby improving software reliability, maintainability, and adaptability.