Advertisement

Preserving specific properties in program development

How to debug programs (Conference version)
  • F. A. Stomp
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

The problem of preserving specific temporal properties in program development is addressed. A new relation between programs, or, more generally, between specifications, is defined. This relation is parameterized by a (finite) collection of temporal properties which will be preserved by that relation. Such a relation will, in general, not preserve all temporal properties. It is proved, however, that for a particular choice of the parameter the new relation coincides with Abadi and Lamport's notion of implements [1], which preserves all (externally visible) temporal properties. As a consequence, the approach for program development proposed in the current paper is as least as powerful as those which use implements as their basic refinement relation. Examples of the latter approaches are those proposed by Back [4], by Lynch and Tuttle [27], and by Lam and Shankar [25]. It is argued that the approach in program development which preserves only certain temporal properties is preferable to those approaches which preserve all temporal properties.

It is shown that the approach advocated here is, except for formally developing programs, also applicable for debugging programs, i.e., for correcting programs which do not satisfy their required specification. This provides -for the first time- a formal basis for “correcting code”.

Keywords

Temporal Property Garbage Collection Execution Sequence Concurrent Program Derivation Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. of the 3rd IEEE Conference on Logic in Computer Science, pages 165–175, 1988.Google Scholar
  2. 2.
    R. J. R. Back. Changing data representation in the refinement calculus. In 21st Hawaii International Conference on System Sciences, 1989.Google Scholar
  3. 3.
    R. J. R. Back. A method for refining atomicity in parallel algorithms. In PARLE89, pages 199–16, 1989.Google Scholar
  4. 4.
    R. J. R. Back. Refinement calculus, part ii: Parallel and reactive programs. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 67–93, 1990.Google Scholar
  5. 5.
    R. J. R. Back and R. Kurki-Suonio. Superposition and fairness in action system refinement. Unpublished Manuscript, 1991.Google Scholar
  6. 6.
    R. J. R. Back and K. Sere. Stepwise refinement of action systems. In Proc. of Math. of Program Construction, volume 375 of LNCS, 1989.Google Scholar
  7. 7.
    R.J.R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.zbMATHMathSciNetCrossRefGoogle Scholar
  8. 8.
    M. Ben-Ari. Algorithms for on-the-fly garbage collection. Transactions of Programming Languages and Systems, 6(3):333–344, 1984.zbMATHCrossRefGoogle Scholar
  9. 9.
    K. M. Chandy and L. Lamport. Distributed snapshots: Determining global states of distributed systems. ACM Trans. on Comp. Syst., 3(1):63–75, 1985.CrossRefGoogle Scholar
  10. 10.
    K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley Publishing Company, Inc., 1988.Google Scholar
  11. 11.
    J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors. Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS. Springer Verlag (Berlin), 1990.Google Scholar
  12. 12.
    E. Diepstraten and R. Kuiper. Abadi & Lamport and Stark: Toward a proof theory for stuttering, dense domains and refinement mappings. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 208–238, 1990.Google Scholar
  13. 13.
    E. W. Dijkstra, L. Lamport, A. J. Martin, C. S. Scholten, and E. F. M. Steffens. On the fly garbage collection: An exercise in cooperation. Communications of the ACM, 21(11):966–975, 1987.CrossRefGoogle Scholar
  14. 14.
    E. W. Dijkstra and C. S. Scholten. Termination detecting for diffusing computations. Information Processing Letters, 11(1):1–4, 1980.zbMATHMathSciNetCrossRefGoogle Scholar
  15. 15.
    E. A. Emerson and Srinivasan J. Branching time temporal logic. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 123–172, 1988.Google Scholar
  16. 16.
    N. Francez. Distributed termination. Transactions of Programming Languages and Systems, 2(1):42–55, 1980.zbMATHCrossRefGoogle Scholar
  17. 17.
    N. Francez. Fairness. Springer Verlag, 1986.Google Scholar
  18. 18.
    R. Gerth. Foundations of compositional program refinement. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 777–808, 1990.Google Scholar
  19. 19.
    C. A. R. Hoare. Proofs of correctness of data representations. Acta Informatica, 1(4):271–281, 1972.zbMATHCrossRefGoogle Scholar
  20. 20.
    C. B. Jones. Software Development. Prentice-Hall International, 1980.Google Scholar
  21. 21.
    B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Department of Computer Science, Uppsala University, Uppsala, Sweden, 1987.Google Scholar
  22. 22.
    S. Katz and D. Peled. Interleaving set temporal logic. In Proc. of the 6th ACM Symposium on Distributed Computing, pages 178–190, 1987.Google Scholar
  23. 23.
    S. Katz and O. Shmueli. Cooperative distributed algorithms for dynamic cycle prevention. IEEE Transactions on Software Engeneering, 13(5):540–552, 1987.zbMATHGoogle Scholar
  24. 24.
    N. Klarlund. Progress Measures and Finite Arguments for Infinite Computations. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, USA, 1990. Also published as Technical Report 90-1153, Cornell University.Google Scholar
  25. 25.
    S. S. Lam and A. U. Shankar. Refinement and projection of relational projections. In J. W. de Bakker, W. P. de Roever, and Rozenberg G., editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 454–487, 1990.Google Scholar
  26. 26.
    L. A. Lynch. Multivalued possibility mappings. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 519–543, 1990.Google Scholar
  27. 27.
    L. A. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. of the 6th ACM Symposium on Distributed Computing, pages 137–151, 1987.Google Scholar
  28. 28.
    Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. foundations of computer science iv, part 2. MC-tracts, 159, 1983.Google Scholar
  29. 29.
    R. Meritt. Completeness theorems for automata. In J. W. de Bakker, W. P. de Roever, and Rozenberg G., editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 544–560, 1990.Google Scholar
  30. 30.
    C. Morgan. The specification statement. Transactions of Programming Languages and Systems, 10(3):403–419, 1988.zbMATHCrossRefGoogle Scholar
  31. 31.
    H. Partsch. Specification and Transformation of Programs — A Formal Approach to Software Development. Springer Verlag (Berlin), 1990.Google Scholar
  32. 32.
    B. Sanders. Stepwise refinement of mixed specifications of concurrent programs. In M. Broy and C. B. Jones, editors, Proceedings of the IFIP TC2 Conference on Programming Concepts and Methods. Elsevier Science Publishers B. V., 1990.Google Scholar
  33. 33.
    K. Sere. Stepwise Refinement of Parallel Programs. PhD thesis, Department of Computer Science, Åbo Akademi, Turku, Finland, 1990.Google Scholar
  34. 34.
    Z. Shengzong. Compositional temporal logic specifications. Technical Report SFB 124-07/1991, Universität des Saarlandes, Deparment of Computer Science, Saarbrücken, Germany, 1991.Google Scholar
  35. 35.
    Z. Shengzong. UNITY-like logic programming. Technical Report SFB 124-06/1991, Universität des Saarlandes, Deparment of Computer Science, Saarbrücken, Germany, 1991.Google Scholar
  36. 36.
    A. K. Singh. Program refinement in fair transition systems. In E. H. L. Aarts, J. van Leeuwen, and M. Rem, editors, Parallel Architectures and Languages Europe 1991, volume 506 of LNCS, pages 128–147, 1991.Google Scholar
  37. 37.
    F. A. Stomp. A derivation of a broadcasting protocol using sequentially phased reasoning. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 696–730, 1990.Google Scholar
  38. 38.
    F. A. Stomp. A derivation of a broadcasting protocol using sequentially phased reasoning (extended abstract). In L. Logrippo, R. L. Probert H., and Ural, editors, Protocol Specification, Testing, and Verification, X. Elsevier Science Publishers B. V. (North-Holland), 1990.Google Scholar
  39. 39.
    F. A. Stomp. Preserving specific properties in program development-How to debug programs-(journal version). In preparation, 1992.Google Scholar
  40. 40.
    F. A. Stomp. Preserving specific properties in program development-How to debug programs-. Technical report, Christian Albrechts Universität, Kiel, Germany, 1992. To appear.Google Scholar
  41. 41.
    J. van de Snepscheut. “Algorithms for on-the-fly garbage collection” revisited. Information Processing Letters, 24(4):211–216, 1987.CrossRefGoogle Scholar
  42. 42.
    J. L. Welch, L. Lamport, and N. A. Lynch. A lattice-structured proof of a minimum spanning tree algorithm. In Proc. of the 7th ACM Symposium on Distributed Computing, pages 28–43, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • F. A. Stomp
    • 1
  1. 1.Institut für Informatik und Praktische Mathematik IIChristian Albrechts UniversitätKielGermany

Personalised recommendations