Advertisement

Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

The correctness of the Schorr-Waite list marking algorithm

Summary

This paper presents a relatively simple proof of a nontrivial algorithm for marking all the nodes of a list structure. The proof separates properties of the algorithm from properties of the data on which it operates and is a significant application of the method of “intermittent assertions”.

This is a preview of subscription content, log in to check access.

References

  1. 1.

    Burstall, R.M.: Proving properties of programs by structural induction. Comput. J. 12, 41–48 (1969)

  2. 2.

    Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. In: Machine intelligence, Vol. 7 (B. Meltzer, D. Michie, eds.), pp. 23–50. Edinburgh: University Press 1972

  3. 3.

    Burstall, R.M.: Program proving as hand simulation with a little induction. In: Proc. IFIP Congress 1974, pp. 308–312. Amsterdam: North-Holland 1974

  4. 4.

    Floyd, R.W.: Assigning meanings to programs. In: Proc. Symposium in Applied Mathematics 19 (J.T. Schwartz, ed.), pp. 19–32. Providence, R.I.: AMS 1967

  5. 5.

    Hoare, C.A.R.: Proof of correctness of data representations. Acta Informat. 1, 271–281 (1972)

  6. 6.

    Knuth, D.W.: The art of computer programming, Vol. 1. Fundamental algorithms. Reading, Mass.: Addison-Wesley 1968

  7. 7.

    Kowaltowski, T.: Correctness of programs manipulating data structures. Ph.D. thesis, University of California, Berkeley, 1973

  8. 8.

    Manna, Z., Waldinger, R.: Is “sometime” sometimes better than “always”? Intermittent assertions in proving program correctness. Comm. ACM 21, 159–172 (1978)

  9. 9.

    Milner, R.: An algebraic definition of simulation between programs. Report No. CS-205, Computer Science Department, Stanford University, 1971

  10. 10.

    Morris, J.H. Jr.: Verification-oriented language design. Technical Report 7, Department of Computer Science, University of California, Berkeley, 1972

  11. 11.

    Poupon, J., Wegbreit, B.: Covering functions. Unpublished report, Centre for Research in Computing Technology, Harvard University, 1972

  12. 12.

    Schorr, H., Waite, W.M.: An efficient machine-independent procedure for garbage collection in various list structures. Comm. ACM 10, 501–506 (1967)

  13. 13.

    Scott, D.: Outline of a mathematical theory of computation. Proc. 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169–176, 1970

  14. 14.

    Suzuki: Automatic verification of programs with complex data structures. Ph.D. thesis, Stanford University, 1976

  15. 15.

    Gries, D.: The Schorr-Waite graph marking algorithm. Acta Informat. 11, 223–232 (1979)

Download references

Author information

Additional information

(This paper grew out of an earlier version which was submitted to this journal on October 16, 1974)

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Topor, R.W. The correctness of the Schorr-Waite list marking algorithm. Acta Informatica 11, 211–221 (1979). https://doi.org/10.1007/BF00289067

Download citation

Keywords

  • Information System
  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory