Skip to main content
SpringerLink
Log in

Deterministic Programs

  • Chapter
Verification of Sequential and Concurrent Programs

Part of the book series: Texts and Monographs in Computer Science ((MCS))

  • 82 Accesses

Abstract

In a deterministic program there is at most one instruction to be executed “next”, so that from a given initial state only one execution sequence is generated. In classical programming languages like Pascal, only deterministic programs can be written. In this chapter we study a small class of deterministic programs, which will be included in all other classes of programs studied in this book.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt. Ten years of Hoare’s logic, a survey, part I. ACM Transactions on Programming Languages and Systems, 3: 431–483, 1981.

    Article  MATH  Google Scholar 

  2. J.W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall International, Englewood Cliffs, NJ, 1980.

    MATH  Google Scholar 

  3. S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7 (1): 70–90, 1978.

    Article  MathSciNet  MATH  Google Scholar 

  4. E.W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs Communications of the ACM, 18: 453–457, 1975.

    Article  MathSciNet  MATH  Google Scholar 

  5. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.

    MATH  Google Scholar 

  6. E.W. Dijkstra. Selected Writings on Computing. Springer-Verlag, New York, 1982.

    MATH  Google Scholar 

  7. F10671 R. Floyd. Assigning meaning to programs In J.T. Schwartz, editor, Proceedings of Symposium on Applied Mathematics 19, Mathematical Aspects of Computer Science, pages 19–32, American Mathematical Society, New York, 1967.

    Google Scholar 

  8. G.A. Gorelick. A complete axiomatic system for proving assertions about recursive and nonrecursive programs Technical Report 75, Department of Computer Science, University of Toronto, 1975.

    Google Scholar 

  9. Gor79] M.J.C. Gordon. The Denotational Description of Programming Languages An Introduction. Springer-Verlag, New York, 1979.

    Google Scholar 

  10. Gri78] D. Gries. The multiple assignment statement. IEEE Transactions on Software EngineeringSE-4:89–93, March 1978.

    Google Scholar 

  11. D. Gries. A note on a standard strategy for developing loop invariants and loops. Science of Computer Programming, 2: 207–214, 1982.

    Article  MathSciNet  MATH  Google Scholar 

  12. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12: 576–580, 583, 1969.

    Google Scholar 

  13. Hoa71] C.A.R. Hoare. Procedures and parameters: an axiomatic approach. In E. Engeler, editor, Proceedings of Symposium on the Semantics of Algorithmic Languages,pages 102–116, New York, 1971. Lecture Notes in Mathematics 188, Springer-Verlag.

    Google Scholar 

  14. HP79] M.C.B. Hennessy and G.D. Plotkin. Full abstraction for a simple programming language. In Proceedings of Mathematical Foundations of Computer Science,pages 108–120, New York, 1979. Lecture Notes in Computer Science 74, Springer-Verlag.

    Google Scholar 

  15. C.A.R. Hoare and N. Wirth. An axiomatic definition of the programming language PASCAL. Acta Informatica, 2: 335–355, 1973.

    Article  Google Scholar 

  16. P.E. Lauer. Consistent formal theories of the semantics of programming languages. Technical Report 25.121, IBM Laboratory Vienna, 1971.

    Google Scholar 

  17. J. Loeckx and K. Sieber. The Foundation of Program Verification. Teubner-Wiley, Stuttgart, second edition, 1987.

    Google Scholar 

  18. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6: 319–340, 1976.

    Article  MathSciNet  MATH  Google Scholar 

  19. E.-R. Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 30: 337–347, 1983.

    Article  MathSciNet  Google Scholar 

  20. G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI-FN 19, Department of Computer Science, Aarhus University, 1981.

    Google Scholar 

  21. J.C. Reynolds. The Craft of Programming. Prentice-Hall International, Englewood Cliffs, NJ, 1981.

    MATH  Google Scholar 

  22. D.S. Scott and C. Strachey. Towards a mathematical semantics for computer languages. Technical Report PRG-6, Programming Research Group, University of Oxford, 1971.

    Google Scholar 

  23. J.E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Mass., 1977.

    Google Scholar 

  24. J.V. Tucker and J.I. Zucker. Program Correctness over Abstract Data Types, with Error-State Semantics. North-Holland and CWI Monographs, Amsterdam, 1988.

    Google Scholar 

  25. J. Zwiers. Compositionality, Concurrency and Partial Correctness — Proof Theories for Networks of Processes and Their Relationship. Lecture Notes in Computer Science 321, Springer-Verlag, New York, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Krzysztof R. Apt

  2. Department of Computer Science, University of Oldenburg, Ammerlander Heerstr. 114-118, 2900, Oldenburg, Germany

    Ernst-Rüdiger Olderog

Authors
  1. Krzysztof R. Apt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer Science+Business Media New York

About this chapter

Cite this chapter

Apt, K.R., Olderog, ER. (1991). Deterministic Programs. In: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4757-4376-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-1-4757-4376-0_3

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4757-4378-4

  • Online ISBN: 978-1-4757-4376-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation