Formal Abstraction of Program Slices for Specification and Requirement Extraction Using Object-Z
Received: 10 July 2025 | Revised: 12 August 2025 | Accepted: 22 August 2025 | Online: 7 January 2026
Corresponding author: K. S. Aparna
Abstract
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.
Keywords:
program slicing, Object-Z representation, requirement extraction, Java systems, software verification, re-engineeringDownloads
References
L. Vidziunas, D. Binkley, and L. Moonen, "The Impact of Program Reduction on Automated Program Repair," in 2024 IEEE International Conference on Software Maintenance and Evolution (ICSME), Flagstaff, AZ, USA, Oct. 2024, pp. 337–349. DOI: https://doi.org/10.1109/ICSME58944.2024.00039
B. Wilber, T. D. Le, and A. Christi, "ReduJavator: A Tool to Simplify Developer-Written Java Unit Tests," in 2024 IEEE International Conference on Data and Software Engineering (ICoDSE), Gorontalo, Indonesia, Oct. 2024, pp. 199–204. DOI: https://doi.org/10.1109/ICoDSE63307.2024.10829914
A. Bianchi, D. Caivano, V. Marengo, and G. Visaggio, "Iterative reengineering of legacy systems," IEEE Transactions on Software Engineering, vol. 29, no. 3, pp. 225–241, Mar. 2003. DOI: https://doi.org/10.1109/TSE.2003.1183932
M. Weiser, "Program Slicing," IEEE Transactions on Software Engineering, vol. SE-10, no. 4, pp. 352–357, Jul. 1984. DOI: https://doi.org/10.1109/TSE.1984.5010248
F. Tip, "A Survey of Program Slicing Techniques," Journal of Programming Languages, vol. 3, pp. 121–189, 1995.
K. B. Gallagher and J. R. Lyle, "Using program slicing in software maintenance," IEEE Transactions on Software Engineering, vol. 17, no. 8, pp. 751–761, Aug. 1991. DOI: https://doi.org/10.1109/32.83912
M. N. Seghir, "Data-Flow Guided Slicing." arXiv, 2018.
Q. Zhang et al., "A Systematic Literature Review on Large Language Models for Automated Program Repair." arXiv, 2024.
J. Singh, P. M. Khilar, and D. P. Mohapatra, "Dynamic slicing of distributed Aspect-Oriented Programs: A context-sensitive approach," Computer Standards & Interfaces, vol. 52, pp. 71–84, May 2017. DOI: https://doi.org/10.1016/j.csi.2017.01.007
H. Agrawal and J. R. Horgan, "Dynamic program slicing," ACM SIGPLAN Notices, vol. 25, no. 6, pp. 246–256, Jun. 1990. DOI: https://doi.org/10.1145/93548.93576
V. D’Silva, D. Kroening, and G. Weissenbacher, "A Survey of Automated Techniques for Formal Software Verification," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 7, pp. 1165–1178, Jul. 2008. DOI: https://doi.org/10.1109/TCAD.2008.923410
X. Chen et al., "Deep learning-based software engineering: progress, challenges, and opportunities," Science China Information Sciences, vol. 68, no. 1, Jan. 2025, Art. no. 111102. DOI: https://doi.org/10.1007/s11432-023-4127-5
I. Brückner and H. Wehrheim, "Slicing Object-Z Specifications for Verification," in ZB 2005: Formal Specification and Development in Z and B, vol. 3455, H. Treharne, S. King, M. Henson, and S. Schneider, Eds. Springer Berlin Heidelberg, 2005, pp. 414–433. DOI: https://doi.org/10.1007/11415787_24
A. Sen and V. K. Garg, "Formal Verification of Simulation Traces Using Computation Slicing," IEEE Transactions on Computers, vol. 56, no. 4, pp. 511–527, Apr. 2007. DOI: https://doi.org/10.1109/TC.2007.1011
B. Homerding et al., "The Parallel Semantics Program Dependence Graph." arXiv, Feb. 01, 2024.
A. Yadavally, T. N. Nguyen, W. Wang, and S. Wang, "(Partial) Program Dependence Learning," in 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), Melbourne, Australia, May 2023, pp. 2501–2513. DOI: https://doi.org/10.1109/ICSE48619.2023.00209
C. Galindo, S. Pérez, and J. Silva, "Program slicing of Java programs," Journal of Logical and Algebraic Methods in Programming, vol. 130, Jan. 2023, Art. no. 100826. DOI: https://doi.org/10.1016/j.jlamp.2022.100826
Z. Guo and Z. Cao, "Combined Formal Modeling and Model Transformation Based on AADL and Object-Z," Journal of Software, pp. 185–199, Nov. 2023. DOI: https://doi.org/10.17706/jsw.18.4.185-199
S. R. Idate, T. S. Rao, and D. J. Mali, "Context-Based Aspect-Oriented Requirement Engineering Model," Engineering, Technology & Applied Science Research, vol. 13, no. 2, pp. 10460–10465, Apr. 2023. DOI: https://doi.org/10.48084/etasr.5699
M. R. Laurence, "Characterizing minimal semantics-preserving slices of function-linear, free, liberal program schemas," The Journal of Logic and Algebraic Programming, vol. 72, no. 2, pp. 157–172, Jul. 2007. DOI: https://doi.org/10.1016/j.jlap.2007.02.008
Downloads
How to Cite
License
Copyright (c) 2025 K. S. Aparna, R. N. Kulkarni
This work is licensed under a Creative Commons Attribution 4.0 International License.
Authors who publish with this journal agree to the following terms:
- Authors retain the copyright and grant the journal the right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) after its publication in ETASR with an acknowledgement of its initial publication in this journal.
