
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Martin Ward, "Derivation of Data Intensive Algorithms by Formal Transformation: The SchnorrWaite Graph Marking Algorithm," IEEE Transactions on Software Engineering, vol. 22, no. 9, pp. 665686, September, 1996.  
BibTex  x  
@article{ 10.1109/32.541437, author = {Martin Ward}, title = {Derivation of Data Intensive Algorithms by Formal Transformation: The SchnorrWaite Graph Marking Algorithm}, journal ={IEEE Transactions on Software Engineering}, volume = {22}, number = {9}, issn = {00985589}, year = {1996}, pages = {665686}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.541437}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Derivation of Data Intensive Algorithms by Formal Transformation: The SchnorrWaite Graph Marking Algorithm IS  9 SN  00985589 SP665 EP686 EPD  665686 A1  Martin Ward, PY  1996 KW  Program development KW  transformation KW  transformational development KW  refinement KW  graph marking KW  SchorrWaite KW  ghost variables KW  data refinement KW  recursion removal KW  pointer switching. VL  22 JA  IEEE Transactions on Software Engineering ER   
Abstract—In this paper, we consider a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program control information with other data structures or which are developed as a combination of a basic idea with an implementation technique. Our approach is based on applying proven semanticspreserving transformation rules in a wide spectrum language. Starting with a set theoretical specification of "reachability," we are able to derive iterative and recursive graph marking algorithms using the "pointer switching" idea of Schorr and Waite. There have been several proofs of correctness of the SchorrWaite algorithm, and a small number of transformational developments of the algorithm. The great advantage of our approach is that we can derive the algorithm from its specification using only generalpurpose transformational rules: without the need for complicated induction arguments. Our approach applies equally well to several more complex algorithms which make use of the pointer switching strategy, including a hybrid algorithm which uses a fixed length stack, switching to the pointer switching strategy when the stack runs out.
[1] J.R. Abrial, S.T. Davis, M.K.O. Lee, D.S. Neilson, P.N. Scharbach, and I.H. Sørensen, The B Method, BP Research, Sunbury Research Centre, U.K., 1991.
[2] J. Arsac, "Transformation of Recursive Procedures," Tools and Notations for Program Construction. D. Neel, ed. Cambridge, U.K.: Cambridge Univ. Press, 1982.
[3] J. Arsac, "Syntactic Source to Source Program Transformations and Program Manipulation," Comm ACM, vol. 22, Jan. 1982.
[4] R.J.R. Back, Correctness Preserving Program Refinements. Mathematical Centre Tracts #131, Mathematisch Centrum, Amsterdam, 1980.
[5] R.J.R. Back and J. von Wright, "Refinement Concepts Formalised in HigherOrder Logic," Formal Aspects of Computing 2, 1990.
[6] R. Balzer, "A 15 Year Perspective on Automatic Programming," IEEE Trans. Software Eng., vol. 11, Nov. 1985.
[7] 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, Feb. 1989.
[8] R. Bird, "Lectures on Constructive Functional Programming," Oxford Univ., Technical Monograph PRG69, Sept. 1988.
[9] M. Broy and P. Pepper, "Combining Algebraic and Algorithmic Reasoning: An Approach to the SchnorrWaite Algorithm," Trans. Programming Languages and Systems, vol. 4, July 1982.
[10] B.A. Davey and H.A. Priestley, Introduction to Lattices and Order.Cambridge, U.K.: Cambridge Univ. Press, 1990.
[11] N. Derschowitz, "The SchnorrWaite Marking Algorithm Revisited," Information Processing Letters, vol. 11, 1980.
[12] R.B.K. Dewar, A. Grand, S.C. Liu, and J.T. Schwartz, "Programming by Refinement as Exemplified by the SETL Representation Sublanguage," ACM Trans. Programming Languages and Systems, vol. 1, July 1979.
[13] E.W. Dijkstra, A Discipline of Programming.Englewood Cliffs, N.J.: Prentice Hall, 1976.
[14] E. Engeler, Formal Languages: Automata and Structures.Chicago: Markham, 1968.
[15] S.L. Gerhart, "A DerivationOriented Proof of the SchnorrWaite Graph Marking Algorithm," Program Construction, G. Goos and H. Hartmanis, eds., Lecture Notes in Computer Science #69,New York, Heidelberg, Berlin: SpringerVerlag, 1979.
[16] D. Gries, "Is Sometimes Ever Better than Always?" Program Construction, G. Goos and H. Harmanis, eds., Lecture Notes in Computer Science #69,New York, Heidelberg, Berlin: SpringerVerlag, 1979.
[17] D. Gries, "The SchnorrWiate Graph Marking Algorithm," Acta Informatica, vol. 11, 1979.
[18] D. Gries, The Science of Programming.New York, Heidelberg, Berlin: SpringerVerlag, 1981.
[19] M. Griffiths, Development of the SchnorrWaite Algorithm, Lecture Notes in Computer Science #69, New York, Heidelberg, Berlin: SpringerVerlag, 1981.
[20] I.J. Hayes, Specification Case Studies.Englewood Cliffs, N.J.: Prentice Hall, 1987.
[21] C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969.
[22] C.B. Jones, Systematic Software Development Using VDM.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[23] C.B. Jones, K.D. Jones, P.A. Lindsay, and R. Moore, mural: A Formal Development Support System.New York, Heidelberg, Berlin: SpringerVerlag, 1991.
[24] Jorring and Scherlis, "Deriving and Using Destructive Data Types," Program Specification and Transformation: Proc. IFIP TC2/WG 2.1 Working Conf., L.G.L.T. Meertens, ed., Bad Tölz, Germany, Apr.1517, 1986.Amsterdam: NorthHolland, 1987.
[25] C.R. Karp, Languages with Expressions of Infinite Length.Amsterdam: NorthHolland, 1964.
[26] D.E. Knuth, "Structured Programming with the GOTO Statement," Computing Surveys, vol. 6, 1974.
[27] R. Kowalski, "Algorithm = Logic + Control," Comm. ACM, vol. 22, July 1979.
[28] Z. Manna and R. Waldinger, "Is 'Sometime' Sometimes Better Than 'Always'? Intermittent Assertions in Proving Program Correctness," Comm. ACM, vol. 21, 1978.
[29] C.C. Morgan, Programming from Specifications, second edition. Englewood Cliffs, N.J.: Prentice Hall, 1994.
[30] J.H. Morris, "A Proof of the SchnorrWaite Algorithm," Theoretical Foundations of Programming Methodology, M. Broy and G. Schmidt, eds., Int'l Summer School, Marktoberdorf, 1981.Dordrecht: Reidel, 1982.
[31] M. Neilson, K. Havelund, K.R. Wagner, and E. Saaman, "The RAISE Language, Method and Tools," Formal Aspects of Computing, vol. 1, 1989.
[32] H. Partsch, "The CIP Transformation System," Program Transformation and Programming Environments, report on a workshop directed by F.L. Bauer and H. Remus, P. Pepper, ed. New York, Heidelberg, Berlin: SpringerVerlag, 1984.
[33] E.L. Post, "Formal Reduction of the General Combinatorial Decision Problem," Am. J. Math., 1943.
[34] W.P. de Roever, "On Backtracking and Greatest Fixpoints," Formal Description of Programming Constructs, E.J. Neuhold, ed. Amsterdam: NorthHolland, 1978.
[35] H. Schnorr and W.M. Waite, "An Efficient MachineIndependent Procedure for Garbage Collection in Various List Structures," Comm. ACM, Aug. 1967.
[36] C.T. Sennett, "Using Refinement to Convince: Lessons Learned from a Case Study," Proc. Refinement Workshop,Hursley Park, Winchester, U.K., Jan.811, 1990.
[37] D. Taylor, "An Alternative to Current Looping Syntax," SIGPLAN Notices, vol. 19, Dec. 1984.
[38] R.W. Topor, "The Correctness of the SchnorrWaite List Marking Algorithm," Acta Informatica, vol. 11, 1979.
[39] M. Ward, "Proving Program Refinements and Transformation," DPhil thesis, Oxford Univ., 1989.
[40] M. Ward, "Derivation of a Sorting Algorithm," technical report, Durham Univ., 1991.
[41] M. Ward, "A Recursion Removal Theorem—Proof and Applications," technical report, Durham Univ., 1991.
[42] M. Ward, "A Resursion Removal Theorem," Proc. Fifth Refinement Workshop,New York, Heidelberg, Berlin: SpringerVerlag, 1992. http://wsmj3.dur.ac.uk/martin/papers/refws5.ps.gz.
[43] M. Ward, "Foundations for a Practical Theory of Program Refinement and Transformation," technical report, Durham Univ., 1994.
[44] M. Ward, "Using Formal Transformations to Construct a Component Repository," Software Reuse: The European Approach.New York, Heidelberg, Berlin: SpringerVerlag, Feb. 1991. http://wsmj3.dur.ac.uk/martin/papers/reuse.ps.gz.
[45] M. Ward, "Abstractign a Specification from Code," J. Software Maintenance: Research and Practice, vol. 5, June 1993.
[46] M. Ward and K.H. Bennett, "A Practical Program Transformation Ssytem for Reverse Engineering," Proc. Working Conf. Reverse Eng.,Baltimore, May2123, 1993. http://wsmj3.dur.ac.uk/martin/papers/icse.ps.gz.
[47] D. Wile, "Type Transformations," IEEE Trans. Software Eng., vol. 7, Jan. 1981.
[48] L. Yelowitz and A.G. Duncan, "Abstractions, Instantiations and Proofs of Marking Algorithms," SIGPLAN Notices, vol. 12, 1977. http://wsmj3.dur.ac.uk/martin/papers/progspec.ps.gz.
[49] E.J. Younger and M. Ward, "Inverse Engineering a Simple Real Time Program," J. Software Maintenance: Research and Practice, vol. 6, 1993.