# Deterministic Programs

Chapter

## 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.

## Keywords

Proof System Proper State Proof Theory Correctness Formula Correctness Proof
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.

## References

- [Apt81]K.R. Apt. Ten years of Hoare’s logic, a survey, part I.
*ACM Transactions on Programming Languages and Systems*, 3: 431–483, 1981.zbMATHCrossRefGoogle Scholar - [Bak80]J.W. de Bakker.
*Mathematical Theory of Program Correctness*. Prentice-Hall International, Englewood Cliffs, NJ, 1980.zbMATHGoogle Scholar - [Coo78]S.A. Cook. Soundness and completeness of an axiom system for program verification.
*SIAM Journal on Computing*, 7 (1): 70–90, 1978.MathSciNetzbMATHCrossRefGoogle Scholar - [Dij75]E.W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs
*Communications of the ACM*, 18: 453–457, 1975.MathSciNetzbMATHCrossRefGoogle Scholar - [Dij76]E.W. Dijkstra.
*A Discipline of Programming*. Prentice-Hall, Englewood Cliffs, N.J., 1976.zbMATHGoogle Scholar - [Dij82]E.W. Dijkstra.
*Selected Writings on Computing*. Springer-Verlag, New York, 1982.zbMATHGoogle Scholar - 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 - [Gor75]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
- Gor79] M.J.C. Gordon.
*The Denotational Description of Programming Languages*An Introduction.*Springer-Verlag, New York, 1979.*Google Scholar - Gri78] D. Gries.
*The multiple assignment statement.*IEEE Transactions on Software Engineering*SE-4:89–93, March 1978.*Google Scholar - [Gri82]D. Gries. A note on a standard strategy for developing loop invariants and loops.
*Science of Computer Programming*, 2: 207–214, 1982.MathSciNetzbMATHCrossRefGoogle Scholar - [Hoa69]C.A.R. Hoare. An axiomatic basis for computer programming.
*Communications of the ACM*, 12: 576–580, 583, 1969.Google Scholar - 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 - 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 - [HW73]C.A.R. Hoare and N. Wirth. An axiomatic definition of the programming language PASCAL.
*Acta Informatica*, 2: 335–355, 1973.CrossRefGoogle Scholar - [Lau71]P.E. Lauer. Consistent formal theories of the semantics of programming languages. Technical Report 25.121, IBM Laboratory Vienna, 1971.Google Scholar
- [LS87]J. Loeckx and K. Sieber.
*The Foundation of Program Verification*. Teubner-Wiley, Stuttgart, second edition, 1987.Google Scholar - [0G76]S. Owicki and D. Gries. An axiomatic proof technique for parallel programs.
*Acta Informatica*, 6: 319–340, 1976.MathSciNetzbMATHCrossRefGoogle Scholar - [01d83]E.-R. Olderog. On the notion of expressiveness and the rule of adaptation.
*Theoretical Computer Science*, 30: 337–347, 1983.MathSciNetCrossRefGoogle Scholar - [Plo81]G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI-FN 19, Department of Computer Science, Aarhus University, 1981.Google Scholar
- [Rey81]J.C. Reynolds.
*The Craft of Programming*. Prentice-Hall International, Englewood Cliffs, NJ, 1981.zbMATHGoogle Scholar - [SS71]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
- [Sto77]J.E. Stoy.
*Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory*. MIT Press, Cambridge, Mass., 1977.Google Scholar - [TZ88]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 - [Zwi89]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

## Copyright information

© Springer Science+Business Media New York 1991