This Article 
 Bibliographic References 
 Add to: 
Derivation of Data Intensive Algorithms by Formal Transformation: The Schnorr-Waite Graph Marking Algorithm
September 1996 (vol. 22 no. 9)
pp. 665-686

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 semantics-preserving 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 Schorr-Waite 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 general-purpose 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 Higher-Order 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 PRG-69, Sept. 1988.
[9] M. Broy and P. Pepper, "Combining Algebraic and Algorithmic Reasoning: An Approach to the Schnorr-Waite 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 Schnorr-Waite 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 Derivation-Oriented Proof of the Schnorr-Waite Graph Marking Algorithm," Program Construction, G. Goos and H. Hartmanis, eds., Lecture Notes in Computer Science #69,New York, Heidelberg, Berlin: Springer-Verlag, 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: Springer-Verlag, 1979.
[17] D. Gries, "The Schnorr-Wiate Graph Marking Algorithm," Acta Informatica, vol. 11, 1979.
[18] D. Gries, The Science of Programming.New York, Heidelberg, Berlin: Springer-Verlag, 1981.
[19] M. Griffiths, Development of the Schnorr-Waite Algorithm, Lecture Notes in Computer Science #69, New York, Heidelberg, Berlin: Springer-Verlag, 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: Springer-Verlag, 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.15-17, 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 Schnorr-Waite 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: Springer-Verlag, 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 Machine-Independent 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.8-11, 1990.
[37] D. Taylor, "An Alternative to Current Looping Syntax," SIGPLAN Notices, vol. 19, Dec. 1984.
[38] R.W. Topor, "The Correctness of the Schnorr-Waite 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: Springer-Verlag, 1992.
[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: Springer-Verlag, Feb. 1991.
[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, May21-23, 1993.
[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.
[49] E.J. Younger and M. Ward, "Inverse Engineering a Simple Real Time Program," J. Software Maintenance: Research and Practice, vol. 6, 1993.

Index Terms:
Program development, transformation, transformational development, refinement, graph marking, Schorr-Waite, ghost variables, data refinement, recursion removal, pointer switching.
Martin Ward, "Derivation of Data Intensive Algorithms by Formal Transformation: The Schnorr-Waite Graph Marking Algorithm," IEEE Transactions on Software Engineering, vol. 22, no. 9, pp. 665-686, Sept. 1996, doi:10.1109/32.541437
Usage of this product signifies your acceptance of the Terms of Use.