Subscribe

Issue No.01 - January/February (2011 vol.37)

pp: 24-47

Martin P. Ward , De Montfort University, Leicester

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.13

ABSTRACT

In this paper, we present a case study in deriving an algorithm from a formal specification via FermaT transformations. The general method (which is presented in a separate paper) is extended to a method for deriving an implementation of a program transformation from a specification of the program transformation. We use program slicing as an example transformation since this is of interest outside the program transformation community. We develop a formal specification for program slicing in the form of a WSL specification statement which is refined into a simple slicing algorithm by applying a sequence of general purpose program transformations and refinements. Finally, we show how the same methods can be used to derive an algorithm for semantic slicing. The main novel contributions of this paper are: 1) developing a formal specification for slicing, 2) expressing the definition of slicing in terms of a WSL specification statement, and 3) by applying correctness preserving transformations to the specification, we can derive a simple slicing algorithm.

INDEX TERMS

Program slicing, program transformations, formal methods, algorithm derivation.

CITATION

Martin P. Ward, "Deriving a Slicing Algorithm via FermaT Transformations",

*IEEE Transactions on Software Engineering*, vol.37, no. 1, pp. 24-47, January/February 2011, doi:10.1109/TSE.2010.13REFERENCES

- [1] T. Amtoft, "Slicing for Modern Program Structures: A Theory for Eliminating Irrelevant Loops,"
Information Processing Letters, vol. 106, pp. 45-51, 2008.- [2] R.J.R. Back, "Correctness Preserving Program Refinements," Math. Centre Tracts#131, Mathematisch Centrum, 1980.
- [3] R.J.R. Back, "A Calculus of Refinements for Program Derivations,"
Acta Informatica, vol. 25, pp. 593-624, 1988.- [4] R.J.R. Back and J. von Wright, "Refinement Concepts Formalised in Higher-Order Logic,"
Formal Aspects of Computing, vol. 2, pp. 247-272, 1990.- [5] F.L. Bauer, B. Moller, H. Partsch, and P. Pepper, "Formal Construction by Transformation—Computer Aided Intuition Guided Programming,"
IEEE Trans. Software Eng., vol. 15, no. 2, pp. 165-180, Feb. 1989.- [6] J.C. Bicarregui and B.M. Matthews, "Proof and Refutation in Formal Software Development,"
Proc. Third Irish Workshop Formal Software Development, July 1999.- [7] G. Bilardi and K. Pingali, "The Static Single Assignment Form and Its Computation," Cornell Univ. technical report, pp. 1-37, http://www.cs.cornell.edu/Info/Projects/ Bernoulli/papersssa.ps, July 1999.
- [8] D. Binkley, "Precise Executable Interprocedural Slices,"
ACM Letters on Programming Languages and Systems, vol. 2, pp. 31-45, Mar. 1993.- [9] D. Binkley, S. Danicic, T. Gyimóthy, M. Harman, Á. Kiss, and B. Korel, "A Formalisation of the Relationship between Forms of Program Slicing,"
Science of Computer Programming, vol. 62, no. 3, pp. 228-252, 2006.- [10] D. Binkley and M. Harman, "A Survey of Empirical Results on Program Slicing,"
Advances in Computers, M. Zelkowitz, ed., vol. 62, Academic Press, 2004.- [11] D. Binkley, M. Harman, and S. Danicic, "Amorphous Program Slicing,"
J. Systems and Software, vol. 68, no. 1, pp. 45-64, Oct. 2003.- [12] D.W. Binkley and K.B. Gallagher, "A Survey of Program Slicing,"
Advances in Computers, vol. 43, pp. 1-52, Academic Press, 1996.- [13] R. Bird and O. de Moor,
The Algebra of Programming. Prentice-Hall, 1996.- [14] Z. Chen, A. Cau, H. Zedan, and H. Yang, "A Refinement Calculus for the Development of Real-Time Systems,"
Proc. Fifth Asia Pacific Software Eng. Conf., 1998.- [15]
Verification, Model Checking, and Abstract Interpretation, R. Cousot, ed. Springer-Verlag, Jan. 2005.- [16] E.W. Dijkstra,
A Discipline of Programming. Prentice-Hall, 1976.- [17] A. Hall, "Seven Myths of Formal Methods,"
IEEE Software, vol. 7, no. 5, pp. 11-19, Sept. 1990.- [18] M. Harman and S. Danicic, "Amorphous Program Slicing,"
Proc. Fifth IEEE Int'l Workshop Program Comprehesion, May 1997.- [19] J. Hatcliff, M.B. Dwyer, and H. Zheng, "Slicing Software for Model Construction,"
J. Higher-Order and Symbolic Computation, vol. 13. no. 4, pp. 315-353, Dec. 2000.- [20] C.A.R. Hoare, I.J. Hayes, H.E. Jifeng, C.C. Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sorensen, J.M. Spivey, and B.A. Sufrin, "Laws of Programming,"
Comm. ACM, vol. 30, no. 8, pp. 672-686, Aug. 1987.- [21] S. Horwitz, T. Reps, and D. Binkley, "Interprocedural Slicing Using Dependence Graphs,"
ACM Trans. Programming Languages and Systems, vol. 12, no. 1, pp. 26-60, Jan. 1990.- [22] C.B. Jones, K.D. Jones, P.A. Lindsay, and R. Moore,
Mural: A Formal Development Support System. Springer-Verlag, 1991.- [23] C.R. Karp,
Languages with Expressions of Infinite Length. North-Holland, 1964.- [24] K.C. Lano and H.P. Haughton, "Formal Development in B,"
Information and Software Technology, vol. 37, pp. 303-316, June 1995.- [25] K. Lano,
The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag, 1996.- [26] M. Mock, D.C. Atkinson, C. Chambers, and S.J. Eggers, "Improving Program Slicing with Dynamic Points-to Data,"
Proc. 10th ACM SIGSOFT Symp. Foundations of Software Eng., pp. 71-80, 2002.- [27] C.C. Morgan, "The Specification Statement,"
ACM Trans. Programming Languages and Systems, vol. 10, pp. 403-419, 1988.- [28] C.C. Morgan,
Programming from Specifications, second ed. Prentice-Hall, 1994.- [29] C.C. Morgan and K. Robinson, "Specification Statements and Refinements,"
IBM J. Research and Development, vol. 31, no. 5, pp. 546-555, 1987.- [30] C.C. Morgan, K. Robinson, and P. Gardiner, "On the Refinement Calculus," Technical Monograph PRG-70, Oxford Univ., Oct. 1988.
- [31] M. Neilson, K. Havelund, K.R. Wagner, and E. Saaman, "The RAISE Language, Method and Tools,"
Formal Aspects of Computing, vol. 1, pp. 85-114, 1989.- [32] R. Paige, "Future Directions in Program Transformations,"
ACM Computing Surveys, vol. 28A, no. 4, pp. 170-174, 1986.- [33] H. Partsch and R. Steinbrügen, "Program Transformation Systems,"
Computing Surveys, vol. 15, no. 3, pp. 199-236, Sept. 1983.- [34] K. Pingali and G. Bilardi, "Optimal Control Dependence Computation and the Roman Chariots Problem,"
ACM Trans. Programming Languages and Systems, vol. 19, no. 3,http://www.cs.cornell.edu/Info/Projects/ Bernoulli/paperstoplas 97.ps, pp. 462-491, May 1997.- [35] H.A. Priestley and M. Ward, "A Multipurpose Backtracking Algorithm,"
J. Symbolic Computation, vol. 18, pp. 1-40, http://www.cse.dmu.ac.uk/~mward/martin/papers backtr-t.ps.gz, 1994, doi:10.1006/jsco.1994.1035. - [36] V. Prasad Ranganath, T. Amtoft, A. Banerjee, M.B. Dwyer, and J. Hatcliff, "A New Foundation For Control-Dependence and Slicing for Modern Program Structures,"
Proc. European Symp. Programming, pp. 77-93, Apr. 2005.- [37] T. Reps, "Algebraic Properties of Program Integration,"
Science of Computer Programming, vol. 17, pp. 139-215, 1991.- [38] T. Reps and W. Yang, "The Semantics of Program Slicing," Computer Sciences Technical Report 777, June 1988.
- [39] N.F. Rodrigues and L.S. Barbosa, "Program Slicing by Calculation,"
J. Universal Computer Science, vol. 12, no. 7, pp. 828-848, 2006.- [40] J.M. Spivey,
The Z Notation: A Reference Manual, second ed. Prentice Hall Int'l, 1992.- [41] B. Steensgaarda, "Points-to Analysis in Almost Linear Time,"
Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, 1996.- [42] S. Stepney, D. Cooper, and J. Woodcock, "More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement,"
The Z Formal Specification Notation, J.P. Bowen, A. Fett, and M.G. Hinchey, eds., pp. 284-307, Springer-Verlag, Sept. 1998.- [43] F. Tip, "A Survey of Program Slicing Techniques,"
J. Programming Languages, vol. 3, no. 3, pp. 121-189, Sept. 1995.- [44] A. Turing, "On Computable Numbers, with an Application to the Entscheidungsproblem,"
Proc. London Math. Soc., vol. 2, no. 42, pp. 230-265, 1936.- [45] G.A. Venkatesh, "The Semantic Approach to Program Slicing,"
Proc. SIGPLAN 1991 Conf. Programming Language Design and Implementation, vol. 26, no. 6, pp. 107-119, June 1991.- [46] M. Ward, "Proving Program Refinements and Transformations," DPhil thesis, Oxford Univ., http://www.cse.dmu.ac.uk/~mward/martinthesis , 1989.
- [47] M. Ward, "Reverse Engineering through Formal Transformation Knuths `Polynomial Addition' Algorithm,"
Computer J., vol. 37, no. 9, pp. 795-813, http://www.cse.dmu.ac.uk/~mward/martin/papers poly-t.ps.gz, 1994, doi:10.1093/comjnl/37.9.795. - [48] M. Ward, "Program Analysis by Formal Transformation,"
Computer J., vol. 39, no. 7, pp. 598-618, http://www.cse.dmu.ac. uk/~mward/martin/ paperstopsort-t.ps.gz, 1996, doi:10.1093/comjnl/39.7.598. - [49] M. Ward, "Assembler to C Migration Using the FermaT Transformation System,"
Proc. Int'l Conf. Software Maintenance, Aug./Sept. 1999.- [50] M. Ward, "Recursion Removal/Introduction by Formal Transformation: An Aid to Program Development and Program Comprehension,"
Computer J., vol. 42, no. 8, pp. 650-673, 1999.- [51] M. Ward, "Reverse Engineering from Assembler to Formal Specifications via Program Transformations,"
Proc. Seventh Working Conf. Reverse Eng., http://www.cse.dmu.ac.uk/~mward/martin/papers wcre2000.ps.gz, Nov. 2000.- [52] M. Ward, "The Formal Transformation Approach to Source Code Analysis and Manipulation,"
Proc. IEEE Int'l Workshop Source Code Analysis and Manipulation, Nov. 2001.- [53] M. Ward, "Abstracting a Specification from Code,"
J. Software Maintenance: Research and Practice, vol. 5, no. 2, pp. 101-122, http://www.cse.dmu.ac.uk/~mward/martin/papers prog-spec. ps.gz, June 1993.- [54] M. Ward, "Specifications from Source Code—Alchemists' Dream or Practical Reality?"
Proc. Fourth Reeng. Forum, Sept. 1994.- [55] M. Ward, "Derivation of Data Intensive Algorithms by Formal Transformation,"
IEEE Trans. Software Eng., vol. 22, no. 9, pp. 665-686, Sept. 1996, doi:doi.ieeecomputersociety.org/10.1109/32.541437. - [56] M. Ward and K.H. Bennett, "A Practical Program Transformation System for Reverse Engineering,"
Proc. IEEE Conf. Software Maintenance-1993, 1993.- [57] M.P. Ward, H. Zedan, and T. Hardcastle, "Conditioned Semantic Slicing via Abstraction and Refinement in FermaT,"
Proc. Ninth European Conf. Software Maintenance and Reeng., Mar. 2005.- [58] M. Ward, "The FermaT Assembler Re-Engineering Workbench,"
Proc. Int'l Conf. Software Maintenance, Nov. 2001.- [59] M. Ward, "Pigs from Sausages? Reengineering from Assembler to C via FermaT Transformations,"
Science of Computer Programming, vol. 52, nos. 1-3, pp. 213-255, Special Issue on Program Transformation, http://www.cse.dmu.ac.uk/~martin/papersmigration-t.ps.gz , 2004, doi:dx.doi.org/10.1016/j.scico.2004. 03.007. - [60] M. Ward, "Properties of Slicing Definitions,"
Proc. Ninth IEEE Int'l Working Conf. Source Code Analysis and Manipulation, Sept. 2009.- [61] M. Ward and H. Zedan, "MetaWSL and Meta-Transformations in the FermaT Transformation System,"
Proc. 29th Ann. Int'l Computer Software and Applications Conf., Nov. 2005.- [62] M. Ward and H. Zedan, "Combining Dynamic and Static Slicing for Analysing Assembler,"
Science of Computer Programming, http://www.cse.dmu.ac.uk/~martin/paperscombined-slicing-t.pdf , 2009, doi:10.1016/j.scico.2009. 11.001. - [63] M. Ward and H. Zedan, "Slicing as a Program Transformation,"
Trans. Programming Languages and Systems, vol. 29, no. 2, pp. 1-52, http://www.cse.dmu.ac.uk/~martin/papersslicing-t.ps.gz , Apr. 2007.- [64] M. Ward, H. Zedan, M. Ladkau, and S. Natelberg, "Conditioned Semantic Slicing for Abstraction; Industrial Experiment,"
Software Practice and Experience, vol. 38, no. 12, pp. 1273-1304, http://www. cse.dmu.ac.uk/~mward/martin/ papersslicing-paper-final.pdf, Oct. 2008, doi:doi.wiley.com/10.1002/spe.869. - [65] M. Weiser, "Program Slicing,"
IEEE Trans. Software Eng., vol. 10, no. 4, pp. 352-357, July 1984.- [66] R.P. Wilson, "Efficient Context-Sensitive Pointer Analysis for C Programs," PhD thesis, Computer Systems Laboratory, Stanford Univ., Dec. 1997.
- [67] R.P. Wilson and M.S. Lam, "Efficient Context-Sensitive Pointer Analysis for C Programs,"
Proc. ACM SIGPLAN 1995 Conf. Programming Language Design and Implementation, June 1995.- [68] N. Wirth, "Program Development by Stepwise Refinement,"
Comm. ACM, vol. 14, no. 4, pp. 221-227, 1971.- [69] J. Wordsworth,
Software Engineering with B. Addison Wesley Longman, 1996.- [70] H. Yang and M. Ward,
Successful Evolution of Software Systems. Artech House, 2003.- [71] E.J. Younger and M. Ward, "Inverse Engineering a Simple Real Time Program,"
J. Software Maintenance: Research and Practice, vol. 6, pp. 197-234, SMART Project, http://www.cse.dmu.ac.uk/~mward/martin/papers eddy-t.ps.gz, 1993, doi:doi.wiley.com/10.1002/smr.4360060404. - [72] X. Zhang, M. Munro, M. Harman, and L. Hu, "Weakest Precondition for General Recursive Programs Formalized in Coq,"
Proc. 15th Int'l Conf. Theorem Proving in Higher Order Logics, 2002.- [73] X. Zhang, M. Munro, M. Harman, and L. Hu, "Mechanized Operational Semantics of WSL,"
Proc. IEEE Int'l Workshop Source Code Analysis and Manipulation (SCAM), 2002. |