Optimizing the SPARK program slicer

ABSTRACT

Recent trends in software re-engineering have included tools to extract program slices from existing Ada procedures. One such tool has already been developed that extracts program slices from SPARK procedures along with a proof that the functionality of the original procedure is equivalent to the functionality of the collection of resulting slices. This paper extends this work by showing how assumptions in the proof can cause inefficiencies in SPARKSlicer and by presenting alternatives that optimize out the inefficiencies. The original proof is modified to show that the SPARK program slicer still produces functionally equivalent program slices from SPARK procedures with these optimizations.

REFERENCES

• 1: ASIS Basic Concepts. Retrieved June 3, 2003, from www.acm.org/sigada/wg/asiswg /basics.html, 1998.
• 2: John Barnes , J. G. Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 3: Dwyer, M. B., Corbett, J.C., Hatcliff, J., Sokolowski, S., and Zheng, H. Slicing Multi-Threaded Java Programs: A Case Study. Tech Report KSU CIS TR 99--7.
• 4: Program Slicing. Retrieved June 4, 2003 from www.ssw.unilinz.ac.at/Research/Projects/ ProgramSlicing.
• 5: SPARK 95 - The SPADE Ada 95 Kernel, copyright Praxis Critical Systems. Edition 4.1, Oct 2003.
• 6: Ricky Eugene Sward, Extracting functionally equivalent object-oriented designs from legacy imperative code, Air Force Institute of Technology, Wright Patterson AFB, OH, 1998
• 7: Ricky E. Sward , A.T. Chamillard, AdaSlicer: an Ada program slicer, Proceedings of the 2003 annual ACM SIGAda international conference on Ada: the engineering of correct and reliable software for real-time & distributed systems using ada and related technologies, p.10-16, December 07-11, 2003, San Diego, CA, USA
• 8: Ricky E. Sward , A. T. Chamillard, Re-engineering global variables in Ada, Proceedings of the 2004 annual ACM SIGAda international conference on Ada: The engineering of correct and reliable software for real-time & distributed systems using Ada and related technologies, p.29-34, November 14-18, 2004, Atlanta, Georgia, USA
• 9: R. E. Sward , T. C. Hartrum, Extracting objects from legacy imperative code, Proceedings of the 12th international conference on Automated software engineering (formerly: KBSE), p.98, November 02-05, 1997
• 10: Sward, R.E. and L.C. Baird III, Proving Functional Equivalence for Program Slicing in SPARK, Lecture Notes in Computer Science 3555, pp 105--114, Ada Europe, Jun 2005, York, England.
• 11: The Unravel Project. Retrieved June 4, 2003, from http://hissa.nist.gov/unravel/, 1998.
• 12: Weiser, M. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352--357, July 1984.
• 13: The Wisconsin Program-Slicing Tool, Version 1.1. Retrieved June 4, 2003, from www.cs.wisc.edu/wpis/slicing_tool/, 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.6 Programming Environments

General Terms:
Languages

Keywords:
ASIS, formal methods, program slicing