- Author:
- C. A. R. Hoare,
- Editor:
- C. B. Jones
Charles Antony Richard Hoare is one of the most productive and prolific computer scientists. This volume contains a selection of his published papers. There is a need, as in a Shakespearian Chorus, to offer some apology for what the book manifestly fails to achieve. It is not a complete 'collected works'. Selection between papers of this quality is not easy and, given the book's already considerable size, some difficult decisions as to what to omit have had to be made. Pity the editor weighing the choice between a seminal paper, perhaps widely republished, and a lesser known gem overtaken by subsequent developments. The only defence that can be offered is to reassure the reader that Tony Hoare was consulted.
The paper published as Chapter 1 is so placed because it provides biographical context. With this exception, the papers appear in chronological order of main publication.
Each paper is introduced by 'link material'. Here again, there is need (at least) for explanation: how can one embellish such papers? The idea behind the link material is to record things which could not have been written in the original paper. Sometimes, it is possible to explain better the context in which a paper was conceived; the subsequent development of the ideas introduced can only be written with hindsight. Apart from these inputs, the papers speak so well for themselves that it has been possible to keep the link material brief. Because the editor's text varies in length, the (abstract and) paper follow immediately rather than being laid out on separate pages. In order to avoid confusion, the link material is set in a smaller fount. Again to assuage the reader's doubts, Hoare does have the last word in the Postscript.
An attempt has been made to trace some of the key dates of drafts, submissions, etc. leading up to publication. For a scientist who points out that 'writing the paper is my method of research' this is both necessary and difficult. Some of Hoare's papers go through many drafts which are circulated to colleagues (sometimes changing title, sometimes using the same title on a complete rewrite.) A complete historiography has not been attempted. In particular, many of Hoare's papers have been reprinted (sometimes in several places): normally, only the first source is given.
With some caution, Hoare's work can be divided under a number of headings. These themes are not disjoint, the whole output comes from a single person. Hoare's work on language definition is seen in Chapters 3, 13, 14, 16 (and also, to a lesser extent, in Chapters 11, 12); his contribution to methods of reasoning about programs is covered in Chapters 4-6, 8, 9, 11, 12, 14, 15, 17, 19, 20; his seminal work on parallelism can be traced through Chapters 10, 12, 15-17. Amidst writing these, often difficult, papers Hoare has produced a number of articles aimed at a wider audience: here, Chapters 1, 2, 7, 18, 21, 22 represent this form of his writing.
The papers themselves have all been re-typeset and only minimal changes have been made. The form of references to other publications has been made uniform and all references have been collected at the end of this volume. In order to provide a useful snapshot, all papers by Hoare (even if there are co-authors) have been gathered into a separate list of references. (Except where they are referred to, Technical Reports etc. are not included: only true 'publications' are listed.) The form of reference to these is '[72]' or 'Hoare([72] )', the list being ordered, and numbers accordingly assigned, on a chronological basis. (This results in the use of 'Hoare' as a key even where the article lists a co-author before Hoare. No disrespect to his erstwhile colleagues is intended.) The other list of references gives works to which Hoare has not contributed. It is listed alphabetically, and references take the form 'Dijksta (1976)', with a, b etc. to distinguish publications in the same year.
The editor and the publishers acknowledge, with thanks, permission to reprint the copyrighted articles in this book that have been published in various journals, proceedings, and books. Individual credits, with details of the sources of the papers, are given as a footnote to each chapter opening.
The task of editing these essays has been most rewarding. The fact that it did not become a burden is largely thanks to the support I have received. I should like to thank Julie Hibbs who has typed and controlled the evolving book; Alison McCauley undertook all of the bibliographic research with real enthusiasm. Thanks are also due to the staff at Prentice Hall International who provided enormous support and encouragement. I am also very grateful to those other computer scientists who have offered advice and/or references. In particular I should like to thank John Reynolds, Jim Horning, Bob Tennant, Brian Randell, David Gries, and Jim King. Finally, I should like to thank Tony Hoare, with whom co-operation is always so stimulating.
Book Downloads
Chapters
- Abelson, H. and Sussman, G. J. (1985) Structure and Interpretation of Computer Programs, MIT Press, Cambridge, Mass.Google Scholar
- Aho, A. V., Hopcraft, J. R. and Ullman, J. D. (1974) The Design and Analysis of Computer Algorithms, Addison-Wesley, Reading, Mass.Google Scholar
- Anderson, D. B. (1973) Private communication.Google Scholar
- Apt, K. R. (1981) Ten years of Hoare's logic, A survey, Part 1, ACM Trans on Programming Languages and Systems, 3(4), 431--83.Google ScholarDigital Library
- ASA Standard COBOL (1968) Codasyl COBOL Journal of Development, National Bureau of Standards Handbook 106 ANSI X 3.23, 1968.Google Scholar
- ASA Standard FORTRAN (1964) Comm. ACM 7(10).Google Scholar
- Atkinson, R. and Hewitt, C. (1976) Synchronisation in actor systems. Working Paper 83, MIT, Cambridge, Mass.Google Scholar
- Backhouse, R. C. (1987) Program Construction and Verification, Prentice Hall, Hemel Hempstead.Google Scholar
- Bakker, J. W. de (1968) Axiomatics of simple assignment statements, MR94, Mathematical Centre, Amsterdam.Google Scholar
- Birtwhistle, G. M., Dahl, O.-J., Myhrhaug, B. and Nygaard, K. (1973) SIMULA BEGIN, Student Literatur, Auerbach.Google Scholar
- Bjørner, D. and Oest, O. N. (1980a) Formal Definition of the Ada Programming Language, INRIA (November).Google Scholar
- Bjørner, D. and Oest, O. N. (1980b) Towards a Formal Description of Ada, Lecture Notes in Computer Science No. 98.Google Scholar
- Brinch Hansen, P. (1972a) A comparison of two synchronizing concepts, Acta Informatica 1, 190--9.Google ScholarDigital Library
- Brinch Hansen, P. (1972b) Structured multiprogramming, Comm. ACM 15(7), 574--8.Google ScholarDigital Library
- Brinch Hansen, P. (1973) Operating System Principles. Prentice Hall, Hemel Hempstead.Google Scholar
- Brinch Hansen, P. (1975) The programming language Concurrent Pascal. IEEE Trans. Software Eng. 1(2), 199--207.Google ScholarDigital Library
- Burstall, R. (1968) Proving properties of programs by structural induction, Experimental Programming Reports, No. 17 DMIP, Edinburgh.Google Scholar
- Burstall, R. M. (1969) Proving programs by structural induction, Comp. J. 12(1), 41--8.Google ScholarCross Ref
- Campbell, R. H. and Habermann, A. N. (1974) The Specification of Process Synchronisation by Path Expressions. Lecture Notes in Computer Science 16, Springer, pp. 89--102.Google Scholar
- Chandy, K. M. and Misra, J. (1988) Parallel Program Design: A Foundation, Addison-Wesley, Reading, Mass.Google Scholar
- Clark, K. L. and McCabe, F. G. (1984) Micro Prolog: Programming in Logic, Prentice Hall, Hemel Hempstead.Google Scholar
- Clint, M. (1973) Program proving: Coroutines, Acta Informatica 2, 50--63.Google ScholarDigital Library
- Cohn, P. M. (1965) Universal Algebra, Harper & Row, New York.Google Scholar
- Conway, M. E. (1963) Design of a separable transition-diagram compiler. Comm. ACM 6(7), 396--408.Google ScholarDigital Library
- Courtois, P. J., Heymans, F. and Parnas, D. L. (1971) Concurrent control with readers and writers. Comm. ACM 14(10), 667--8.Google ScholarDigital Library
- Courtois, P. J., Heymans, F. and Parnas, D. L. (1972) Comments on Courtois et al. (1971). Acta Informatica, 1, 375--6.Google ScholarDigital Library
- Dahl, O.-J. (1972) Hierarchical program structures. In Dahl et al. ([29]).Google Scholar
- Dahl, O.-J. et al. (1967) SIMULA 67, Common Base Language, Norwegian Computing Centre, Forskningveien, Oslo.Google Scholar
- Dahl, O.-J., Myhrhaug, B., Nygaard, K. (1970) The Simula 67 Common Base Language, Norwegian Computing Centre, Oslo, Publication No. S-22.Google Scholar
- Darlington, J. and Burstall, R. M. (1973) A system which automatically improves programs. In Proceedings of Third International Conference on Artifical Intelligence 479--85, Stanford, California.Google Scholar
- Dijkstra, E. W. (1968a) A constructive approach to the problem of program correctness, BIT 8, 174--86.Google ScholarDigital Library
- Dijkstra, E. W. (1968b) Cooperating sequential processes. In Genuys, F. (ed.), Programming Languages, Academic Press, New York, pp. 43--112.Google Scholar
- Dijkstra, E. W. (1972a) A class of allocation strategies inducing bounded delays only. Proc AFIPS SJCC, 40, 933--6, AFIPS Press, Montvale, N.J.Google Scholar
- Dijkstra, E. W. (1972b) Hierarchical ordering of sequential processes. In Hoare, C. A. R. and Perrott, R. H. (eds.) [20].Google Scholar
- Dijkstra, E. W. (1972c) Notes on structured programming. In Dahl et al. ([29]), pp. 1--82.Google Scholar
- Dijkstra, E. W. (1972d) Information streams sharing a finite buffer. Information Processing Letters 1(5), 179--80.Google ScholarCross Ref
- Dijkstra, E. W. (1975a) Guarded commands, nondeterminacy, and formal derivation of programs. Comm. ACM 18(8), 453--7.Google ScholarDigital Library
- Dijkstra, E. W. (1975b) Verbal communication, Marktoberdorf.Google Scholar
- Dijkstra, E. W. (1976) A Discipline of Programming, Prentice Hall, Hemel Hempstead.Google Scholar
- Floyd, R. W. (1967) Assigning meanings to programs, Proc. Amer. Soc. Symp. Appl. Math. 19, 19--31.Google ScholarCross Ref
- Foley, M. (1969) Proof of the Recursive Procedure Quicksort: a Comparison of Two Methods, Master's Dissertation, Queen's University of Belfast.Google Scholar
- Gries, D. (1978) (ed.) Programming Methodology, Springer-Verlag, New York.Google Scholar
- Gries, D. (1981) The Science of Programming, Springer-Verlag, New York.Google Scholar
- Hayes, I. (ed.) (1987) Specification Case Studies, Prentice Hall, Hemel Hempstead.Google Scholar
- Hehner, E. C. R. (1984) Predicative programming, Part 1, Comm. Ass. Comput. Mach. 27(2), 134--43.Google ScholarDigital Library
- Henderson, P. (1980) Functional Programming: Application and Implementation, Prentice Hall, Hemel Hempstead.Google Scholar
- Igarishi, S. (1968) An axiomatic approach to equivalence problems of algorithms with applications, Ph.D. Thesis, 1964. Rep. Compt. Centre, University of Tokyo, pp. 1--101.Google Scholar
- Jones, C. B. (1971) Formal Development of Correct Algorithms. An example based on Earley's Recogniser. Proc. ACM SIGPLAN Conf. Proving Assertions about Programs, 150--69.Google Scholar
- Jones, C. B. (1983) Specification and design of (parallel) programs. In Mason (1983).Google Scholar
- Jones, C. B. (1986) Systematic Software Development Using VDM, Prentice Hall, Hemel Hempstead.Google Scholar
- Jones, G. (1987) Programming in OCCAM, Prentice-Hall, Hemel Hempstead.Google Scholar
- Kahn, G. (1974) The semantics of a simple language for parallel programming. In Proc. IFIP Congress 74, North-Holland.Google Scholar
- King, J. C. (1969) A Program Verifier, Ph.D. Thesis, Carnegie-Mellon University, Pittsburg, Pa.Google Scholar
- Kleene, S. C. (1952) Introduction to Metamathematics, Van Nostrand.Google Scholar
- Knuth, D. E. (1967) Remaining troublespots in ALGOL60, Comm, ACM 10(10).Google Scholar
- Knuth, D. E. (1973) A Review of Structured Programming, CS-73-371, Department of Computer Science, Stanford University:Google Scholar
- Knuth, D. E. (1974) Structured programming with GOTO statements, Technical Report, Computer Science Dept, Stanford University, STAN-CS-74-416.Google Scholar
- Knuth, D. E. (1973) The Art of Computer Programming, Vols 1, 2 & 3, Addison-Wesley, Reading, Mass.Google Scholar
- Kowalski, R. (1979) Logic for Problem Solving, North-Holland, Amsterdam.Google Scholar
- Laski, J. (1968) Sets and other types, ALGOL Bull 27.Google Scholar
- Liskov, B. H. (1974) A Note on CLU. Computation Structures Group Memo. 112, MIT, Cambridge, Mass.Google Scholar
- McBride, F. V., Morrison, D. J. T. and Pengelby, R. M. (1970) A symbol manipulation system. In Machine Intelligence, Vol. 5, Edinburgh University Press.Google Scholar
- McCarthy, J. (1960) Recursive functions of symbolic expressions and their computation by machine, Part 1, Comm ACM 3(4), 184--95.Google ScholarDigital Library
- McCarthy, J. (1963a) A basis for a mathematical theory of computation. In Braffort, P. and Hirschberg, D. (eds), Computer Programming and Formal Systems, North-Holland, Amsterdam.Google Scholar
- McCarthy, J. (1963b) Towards a mathematical theory of computation, Proc. IFIP Cong., 1962, North-Holland, Amsterdam.Google Scholar
- McIlroy, M. D. (1968) Coroutines, Bell Laboratories, Murray Hill, N.J.Google Scholar
- Martin, J. J. (1986) Data Types and Data Structures, Prentice Hall, Hemel Hempstead.Google Scholar
- Mason, R. E. A. (ed.) (1983), Information Processing '83, Elsevier Science Publishers B. V. (North-Holland) IFIP.Google Scholar
- Michie, D. (1967) Memo functions: a language feature rote 'with learning' properties, Report MIP-R-29, Edinburgh University.Google Scholar
- Milner, A. J. R. G. (1971) An Algebraic Definition of Simulation Between Programs. Stanford Computer Science Dept. CS205.Google Scholar
- Milner, A. J. R. G. (1980) A Calculus of Communicating Systems. Springer LNCS Vol. 92, Springer-Verlag, Berlin.Google Scholar
- Misra, J. and Gries, D. (1978) A linear sieve algorithm for finding prime numbers, ACM 21(12), 999--1003.Google ScholarDigital Library
- Morris, F. L. and Jones, C. B. (1984) An early program by Alan Turing, Annals of the History of Computing, 6(2).Google ScholarDigital Library
- Naur, P. (1960) (ed), Report on the algorithmic language ALGOL 60, Comm. ACM 3(5), 299--314; Num. Math., 106--36.Google ScholarDigital Library
- Naur, P. (1963) (ed.): Revised report on the algorithmic language ALGOL 60. Comm. ACM 6, 1--17; Comp. J. 5, 349--67 (1962/63); Numer. Math. 4, 420--453 (1963).Google ScholarDigital Library
- Naur, P. (1966) Proof of algorithms by general snapshots, BIT 6(4), 310--16.Google ScholarCross Ref
- Naur, P. (1969) Programming by action clusters, BIT 9(3) 250--8.Google ScholarCross Ref
- Nipkow, T. (1986) Non-deterministic data types: models and implementations, Acta Informatica 22, 629--61.Google ScholarDigital Library
- PL/I Language Specifications, IBM Order Number GY33-6003-2.Google Scholar
- Pritchard, P. (1981) A sublinear sieve algorithm for finding prime numbers, ACM 24(1), 18--23.Google ScholarDigital Library
- Pritchard, P. (1987) Linear prime-number sieves: a family tree, Science of Computer Programming, 9(1).Google Scholar
- Reynolds, J. C. (1965) COGENT. ANL-7022, Argonne Nat. Lab., Argonne, Ill.Google Scholar
- Reynolds, J. C. (1981) The Craft of Programming, Prentice Hall, Hemel Hempstead.Google Scholar
- Ross, D. T. (1961) A generalized technique for symbol manipulation and numerical calculation, Comm. ACM (March).Google Scholar
- Samelson, K. (1965) Functionals and Functional Transformations, ALGOL Bulletin 20, pp. 27--8.Google Scholar
- Schwartz, S. T. (ed.) (1967) Mathematical Aspects of Computer Science, American Mathematical Society, Providence.Google Scholar
- Scott, D. S. (1970), Outline of a Mathematical Theory of Computation, PRG-2. Programming Research Group, Oxford University.Google Scholar
- Scott, D. S. (1971) The lattice of flow diagrams. In Engeler, E., (ed.), Symposium on Semantics of Algorithmic Languages, Springer Verlag.Google ScholarCross Ref
- Scott, D. S. (1981) Lecture Notes on a Mathematical Theory of Computation. PRG 19, p. 148. Oxford University Computing Laboratory.Google Scholar
- Steel, T. B. (ed.) (1966) Formal Language Description Languages for Computer Programming, North-Holland, Amsterdam.Google Scholar
- Stoy, J. (1977) Denotational Semantics: The Scott--Strachey Approach to Programming Language Theory, MIT Press, Cambridge, Mass.Google Scholar
- Thompson, K. (1976) The UNIX command language. In Structured Programming, Infotech, Nicholson House, Maidenhead, England, pp. 375--84.Google Scholar
- Turing, A. M. (1949) Checking a large routine, Report on a Conference on High Speed Automatic Calculating Machines, University Math. Lab., Cambridge, pp. 67--9.Google Scholar
- Waldinger, R. and Levitt, K. N. (1973) Reasoning about programs. In Proceedings of ACM Sigact/Sigplan Symposium on Principles of Programming Language Design, Boston.Google ScholarDigital Library
- Welsh, J. and McKeag, M. (1980) Structured System Programming, Prentice Hall, Hemel Hempstead.Google Scholar
- Welsh, J. and Quinn, C. (1972) A PASCAL compiler for the ICL 1900 Series Computers. Software, Practice and Experience 2, 73--7.Google ScholarCross Ref
- Wijngaarden, A. van (1965) Orthogonal Design and Description of a Formal Language, MR76, Mathematical Centre, Amsterdam (October).Google Scholar
- Wijngaarden, A. van (1966) Numerical analysis as an independent science, BIT 6, 66--81.Google ScholarCross Ref
- Wijngaarden, A. van (1969) (ed.) Report on the algorithmic language ALGOL 68. Num. Math. 14, 79--218.Google ScholarDigital Library
- Wirth, N. (1965) Proposal for a Report on a Successor of ALGOL60, MR75, Mathematical Centre, Amsterdam, August 1965.Google Scholar
- Wirth, N. (1968) PL/360, JACM 15(1).Google Scholar
- Wirth, N. (1971a) The design of a Pascal compiler. Software, Practice and Experience 1, 309--33.Google ScholarCross Ref
- Wirth, N. (1971b) Program development by stepwise refinement, Comm. ACM 14(4), 221--7.Google ScholarDigital Library
- Wirth, N. (1971c) The programming language PASCAL, Acta Informatica, 1(1), 35--63.Google ScholarDigital Library
- Wirth, N. (1973) Systematic Programming: An Introduction, Prentice Hall, Hemel Hempstead.Google Scholar
- Wirth, N. and Weber, (1966) Comm. ACM, 9(2), 89.Google ScholarDigital Library
- Wulf, W. A., London, R. L. and Shaw, M. (1976) Abstraction and Verification in ALPHARD. Dept. of Computer Science, Carnegie-Mellon University, Pittsburgh, Pa.Google Scholar
- Yanov, Yu, I. (1958) Logical operator schemes, Kybernetika 1.Google Scholar
- Iu. Ia. Basilevskii (ed.). Theory of Mathematical Machines, Pergamon Press (1961). Translated from Russian by C. A. R. Hoare.Google Scholar
- C. A. R. Hoare. [Reference contains text which could not be captured.] (1961). In Foreign Develop. Mach. Translat. Info. Proc. No. 95 (Translated from Mashinnii Perevod i Prikladnaya Lingvistika No. 6, pp. 80--8).Google Scholar
- C. A. R. Hoare. Algorithm 63, Partition; Algorithm 64, Quicksort; Algorithm 65, Find. Communications of the ACM, 4(7), 321--2 (1961).Google Scholar
- C. A. R. Hoare. Quicksort. BCS, Computer Journal, 5(1), 10--15(1962). Chapter 2 of the current book.Google Scholar
- C. A. R. Hoare. Report on the Elliott ALGOL translator, BCS, Computer Journal, 5(2), 127--9 (July 1962).Google Scholar
- C. A. R. Hoare. The Elliott ALGOL input/output system. BCS, Computer Journal, 5(4), 345--8 (January 1963).Google Scholar
- C. A. R. Hoare. The Elliott ALGOL programming system. In P. Wegner (ed.), Introduction to Systems Programming, Academic Press (1964), pp. 156--66.Google Scholar
- C. A. R. Hoare. A note on indirect addressing. ALGOL Bulletin, 21, 63--5 (November 1965).Google Scholar
- N. Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Communications of the ACM, 9(6), 413--32 (June 1966). Chapter 3 of the current book.Google Scholar
- C. A. R. Hoare. Single pass compilation. PL/I. In Proceedings of the ACTP Summer School on Software (June 1966).Google Scholar
- C. A. R. Hoare. Record handling. In F. Genuys (ed.) Programming Languages, Academic Press, 1968, pp. 291--397.Google Scholar
- C. A. R. Hoare. Limitations on languages. Computer Weekly (1968).Google Scholar
- C. A. R. Hoare. Critique of ALGOL 68, Algol Bulletin, 29, 27--9 (November 1968).Google Scholar
- C. A. R. Hoare. Date structures in two-level store. In Proceedings of the IFIP Congress, Edinburgh, 1968, North-Holland (1969), pp. 322--9.Google Scholar
- C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM 12(10), 576--80, 583 (October 1969) Chapter 4 of the current book.Google Scholar
- C. A. R. Hoare. Proof of a program: FIND. Comm. ACM, 14(1), 39--45 (January 1971) Chapter 5 of the current book.Google Scholar
- C. A. R. Hoare. Procedures and parameters: an axiomatic approach. In E. Engeler (ed.), Symposium On Semantics of Algorithmic Languages. Lecture Notes in Mathematics 188, Springer-Verlag (1971), pp. 102--16. Chapter 6 of the current book.Google Scholar
- C. A. R. Hoare. Computer Science. New Lecture Series 62, 1971. Chapter 7 of the current book.Google Scholar
- M. Foley and C. A. R. Hoare. Proof of a recursive program: QUICKSORT. BCS, Computer Journal, 14(4), 391--5 (November 1971).Google Scholar
- C. A. R. Hoare and R. H. Perrott. Operating System Techniques. Academic Press, 1972.Google Scholar
- C. A. R. Hoare. Operating systems: their purpose, objectives, functions and scope. In [20], pp. 11--28Google Scholar
- C. A. R. Hoare. Towards a theory of parallel programming. In [20], pp. 61--71.Google Scholar
- C. A. R. Hoare and R. M. McKeag. A survey of store management techniques: part 1. In [20], pp. 117--31Google Scholar
- C. A. R. Hoare and R. M. McKeag. A survey of store management techniques: Part 2. In [20], pp. 132--51Google Scholar
- C. A. R. Hoare. Prospects for a better programming language. Infotech State of the Art Report: High Level Languages, 7, 327--43 (1972).Google Scholar
- M. Clint and C. A. R. Hoare. Program proving: jumps and functions. Acta Informatica 1(3), 214--24 (1972).Google Scholar
- C. A. R. Hoare. The quality of software. Software Practice and Experience, 2(2), 103--5 (April 1972).Google Scholar
- C. A. R. Hoare and D. C. S. Allison. Incomputability. ACM, Computing Surveys, 4(3), 169--78 (September 1972).Google Scholar
- O.-J. Dahl, E. W. Dijkstra, and C. A. R. Hoare (eds.) Structured Programming. Academic Press, 1972.Google Scholar
- C. A. R. Hoare. Notes on data structuring. In [29], pp. 83--174.Google Scholar
- O.-J. Dahl and C. A. R. Hoare. Hierarchical program structures. In [29], pp. 175--220.Google Scholar
- C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4), 271--81(1972) Chapter 8 of the current book.Google Scholar
- C. A. R. Hoare. A Note on the FOR Statement. BIT, 12(3), 334--41 (1972).Google Scholar
- C. A. R. Hoare. Proof of a structured program: 'The Sieve of Eratosthenes'. BCS, Computer Journal, 15(4); 321--5 (November 1972). Chapter 9 of the current book.Google Scholar
- C. A. R. Hoare. A general conservation law for queueing disciplines. Information Processing Letters, 2(3), 82--5 (August 1973).Google Scholar
- C. A. R. Hoare. A structured paging system. BCS, Computer Journal, 16(3), 209--15 (August 1973). Chapter 10 of the current book.Google Scholar
- C. A. R. Hoare and N. Wirth. An axiomatic definition of the programming language PASCAL. Acta Informatica, 2(4), 335--55 (1973). Chapter 11 of the current book.Google Scholar
- C. A. R. Hoare. Tomorrow's men: the role of the university. Computer Weekly, Educational Supplement, 7 (26 July 1973).Google Scholar
- C. A. R. Hoare. Computer programming as an engineering discipline. Electronics and Power, 19(14); 316--20 (August 1973).Google Scholar
- C. A. R. Hoare. High level programming languages, the way behind. In Simpson, D. (ed.), High Level Programming Languages -- The Way Ahead, NCC Publications, Manchester (1973).Google Scholar
- C. A. R. Hoare and P. E. Lauer. Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica, 3(2), 135--53 (1974).Google Scholar
- C. A. R. Hoare. Monitor: an operating system structuring concept. Communications of the ACM, 17(10), 549--57 (October 1974). Chapter 12 of the current book.Google Scholar
- C. A. R. Hoare. Hints on programming language design. In Bunyan, C. J. (ed.), State of the Art Report 20: Computer Systems Reliability, Pergamon/Infotech (1974), pp. 505--34. Chapter 13 of the current book.Google Scholar
- C. A. R. Hoare. Optimisation of store size for garbage collection. Information Processing Letters, 2(6), 165--6 (April 1974).Google Scholar
- C. A. R. Hoare. Software design: a parable. Software World, 5(9--10), 53--6 (1974).Google Scholar
- C. A. R. Hoare. Program correctness proofs. In Shaw, B. (ed.), Formal Aspects of Computing Science, Newcastle upon Tyne, 3--6 September, 1974 (1975), pp. 7--45.Google Scholar
- C. A. R. Hoare and H. C. Johnston. Matrix reduction -- an efficient method (school timetables). Communications of the ACM, 18(3), 141--50 (March 1975).Google Scholar
- P. H. Enslow, C. A. R. Hoare, J. Palme, D. Parnas, and I. Pyle. Implementation Languages for Real-Time Systems -- I. Standardisation -- its Implementation and Acceptance. Report No. ERO-2-75-Vol. 1, European Res. Office, London, UK (15 April 1975).Google Scholar
- P. H. Enslow, C. A. R. Hoare, J. Palme, D. Parnas, and I. Pyle. Implementation Languages for Real-Time Systems -- II. Language Design -- General Comments. Report No. ERO-2-75-Vol. 2, European Res. Office, London, UK (15 April 1975).Google Scholar
- P. H. Enslow, C. A. R. Hoare, J. Palme, D. Parnas, and I. Pyle. Implementation Languages for Real-Time Systems -- III. Command and Control Languages -- Specific Comments. Report No. ERO-2-75-Vol. 3, European Res. Office, London, UK (15 April 1975).Google Scholar
- C. A. R. Hoare. Recursive data structures. International Journal of Computer and Information Sciences, 4(2), 105--32 (June 1975). Chapter 14 of the current book.Google Scholar
- C. A. R. Hoare. Parallel programming: an axiomatic approach. Computer Languages, 1(2), 151--60 (June 1975). Chapter 15 of the current book.Google Scholar
- C. A. R. Hoare. Date reliability. In Int. Conf. Reliable Software, Los Angeles, pp. 528--33, ACM SIGPLAN Notices (June 1975).Google ScholarDigital Library
- C. A. R. Hoare. Software engineering. BCS, Computer Bulletin, 2(6), 6--7 (December 1975).Google Scholar
- W. H. Kaubisch, R. H. Perrott, and C. A. R. Hoare. Quasiparallel programming. Software Practice and Experience, 6(3); 341--56 (July 1976).Google Scholar
- C. A. R. Hoare, Structured programming in introductory programming courses. Infotech, Structured Programming, 255--63 (1976).Google Scholar
- C. A. R. Hoare. The high cost of programming languages. Software Systems engineering, 413--29 (1976).Google Scholar
- C. A. R. Hoare. The structure of an operating system. In Language Hierarchies and Interfaces, Springer-Verlag (1976), pp. 242--65.Google ScholarCross Ref
- E. A. Ashcroft, K. Clint, and C. A. R. Hoare. Remarks on 'program proving: jumps and functions'. Acta Information, 6(3), 317--18 (1976).Google Scholar
- C. A. R. Hoare. Hints on the design of a programming language for real-time command and control. In Spencer J. P. (ed.), Real-time Software: International State of the Art Report, Infotech International (1976), pp. 685--99.Google Scholar
- A. M. MacNaughten and C. A. R. Hoare. Fast fourier transform free from tears. BCS, Computer Journal, 20(1), 78--83 (February 1977).Google Scholar
- C. A. R. Hoare. Introduction. In Perrott, R. H. (ed.), Software Engineering --- Proceedings of a Symposium held at the Queen's University of Belfast 1976 Academic Press (1977), pp. 7--14 (APIC Studies in Data Processing No. 14).Google Scholar
- J. Welsh, W. J. Sneeringer, and C. A. R. Hoare. Ambiguities and insecurities in PASCAL. Software Practice and Experience, 7(6), 685--96 (November--December 1977).Google Scholar
- C. A. R. Hoare. Software engineering: a keynote address. In 3rd International Conference on Software Engineering, Atlanta, GA., USA, 10--12 May (1978), pp. 1--4.Google Scholar
- C. A. R. Hoare. Some properties of predicate transformers. Journal of the ACM, 25(3), 461--80 (July 1978).Google Scholar
- C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8), 666--77 (August 1978). Chapter 16 of the current book.Google Scholar
- C. A. R. Hoare. Communicating sequential processes. In Shaw, B. (ed.) Digital Systems Design. Proceedings of the Joint IBM University of Newcastle upon Tyne Seminar, 6--9 September 1977, Newcastle University (1978), pp. 145--56.Google Scholar
- N. Francez, C. A. R. Hoare, D. J. Lehmann, and W. P. de Roever. Semantics of nondeterminism, concurrency and communication. Journal of Computer and System Sciences, 19(3), 290--308 (December 1979).Google Scholar
- C. A. R. Hoare. A model for communicating sequential processes. In McKeag, R. M. and MacNaughten, A. M. (eds.), On the Construction of Programs, Cambridge University Press (1980), pp. 229--54.Google Scholar
- C. A. R. Hoare and J. R. Kennaway. A theory of non-determinism. In Proceedings ICALP '80, Springer-Verlag, Lecture Notes In Computer Science, No. 85 (1980), pp. 338--50.Google Scholar
- C. A. R. Hoare. Hoare on programming. Computer World UK (22 October 1980). Text of an interview.Google Scholar
- C. A. R. Hoare. Synchronisation of parallel processes. In Hanna, F. K. (ed.), Advanced Techniques for Microprocessor Systems, Peter Peregrinus (1980), pp. 108--11.Google Scholar
- C. A. R. Hoare. The emperor's old clothes. Communications of the ACM, 24(2), 75--83 (February 1981). Chapter 1 of the current book.Google Scholar
- Zhou Chao Chen and C. A. R. Hoare. Partial correctness of communicating sequential processes. In Proceedings of 2nd International Conference on Distributed Computing Systems, IEEE Computer Society Press (8--10 April 1981), pp. 1--12.Google Scholar
- C. A. R. Hoare and Zhou Chao Chen. Partial Correctness of Communicating Processes and Protocols. Technical Report PRG 20, Oxford University Computing Laboratory, Programming Research Group (May 1981).Google Scholar
- C. A. R. Hoare. A calculus of total correctness for communicating processes. The Science of Computer Programming, 1(1--2), 49--72 (October 1981). Chapter 17 of the current book.Google Scholar
- C. A. R. Hoare. Professionalism. BCS, Computer Bulletin, 2(29), 2--4 (1981). Invited Talk given at BCS 81.Google Scholar
- C. A. R. Hoare. Is there a mathematical basis for computer programming? NAG Newsletter, 2, 6--15 (1981).Google Scholar
- C. A. R. Hoare and Zhou Chao Chen. The Consistency of the Calculus of Total Correctness for Communicating Processes. PRG Monograph 26, Oxford University Computing Laboratory, Programming Research Group (February 1982).Google Scholar
- C. A. R. Hoare and R. M. McKeag, Structure of an operating system. In Broy, M. and Schmidt, G. (eds.), Theoretical Foundations of Programming Methodology -- Lecture Notes of an International Summer School, Germany, 1981, Reidel (1982), pp. 643--58.Google Scholar
- W. H. Kaubisch and C. A. R. Hoare. Discrete event simulation based on communicating sequential processes. In Broy, M. and Schmidt, G. (eds.), Theoretical Foundations of Programming Methodology -- Lecture Notes of an International Summer School, Germany, 1981, Reidel (1982). pp. 625--42.Google Scholar
- C. A. R. Hoare. Specifications, Programs and Implementations. Technical Report PRG-29, ISBN 0-902928-17-1, Programming Research Group, Oxford University (June 1982).Google Scholar
- C. A. R. Hoare. Programming is an engineering profession. In Wallis, P. J. L. (ed.), State of the Art Report 11, No. 3: Software Engineering, Pergamon/Infotech (1983), pp. 77--84. Also Oxford PRG Monograph No. 27.; and IEEE Software 1(2). Chapter 18 of the current book.Google Scholar
- C. A. R. Hoare and E. R. Olderog. Specification-oriented semantics for communicating processes. In Automata Languages and Programming 10th Colloquium, Springer-Verlag (1983), pp. 561--72.Google Scholar
- C. A. R. Hoare. Notes on Communicating Sequential Processes. Monograph 33, Oxford University Computing Laboratory, Programming Research Group (August 1983).Google Scholar
- E. R. Olderog and C. A. R. Hoare. Specification-oriented semantics for communicating processes. In Diaz, J. (ed.), Automata, Languages and Programming -- Proceedings of the 10th International Colloquium, Barcelona July 18--22. Lecture Notes in Computer Science 154, Springer-Verlag (1983) pp. 561--72.Google Scholar
- C. A. R. Hoare. 1983 technology forecast. Electronic Design (January 1983).Google Scholar
- E. C. R. Hehner and C. A. R. Hoare. A more complete model of communicating processes. Theoretical Computer Science, 26(1--2), 105--20 (September 1983).Google Scholar
- C. A. R. Hoare. Programming: sorcery or science. IEEE Software, 1(2), 5--16 (April 1984).Google Scholar
- S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3), 560--99 (July 1984).Google Scholar
- C. A. R. Hoare and A. W. Roscoe. Programs as executable predicates. In Proceedings of the International Conference on Fifth Generation Computer Systems, November 6--9 1984, Tokyo, Japan, ICOT (1984), pp. 220--8Google Scholar
- C. A. R. Hoare. Notes on communicating systems. In Broy, M. (ed.), Control Flow and Data Flow: Concepts of Distributed Programming. Proceedings of NATO Advanced Study Institute International Summer School, Marktoberdorf, 31 July-12 August, 1984, Springer-Verlag (1985), pp. 123--204.Google Scholar
- C. A. R. Hoare. A couple of novelties in the propositional calculus. Zeitschr. f. Math. Logik und Grundlagen d. Math., 31(2), 173--8 (1985). Chapter 19 of the current book.Google Scholar
- C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall (1985). 256 pages, ISBN 0-13-153271-5.Google Scholar
- C. A. R. Hoare and J. C. Shepherdson (eds.) Mathematical Logic and Programming Languages. Prentice Hall (1985). ISBN 0-13-561465-1. The papers in this book were first published in the Philosophical Transactions of the Royal Society, Series A, 312 (1984).Google Scholar
- C. A. R. Hoare. Programs are predicates. In Hoare, C. A. R. and Shepherdson, J. C. (eds.), Mathematical Logic and Programming Languages, Prentice Hall (1985), pp. 141--54. Chapter 20 of the current book.Google Scholar
- H3.M.S4. Data refinement refined (May 1985) Typescript, Programming Research Group, Oxford University.Google Scholar
- C. A. R. Hoare and C. Morgan. Specification of a simplified network service in CSP. In Denvir, B. T., Harwood, W. T. and Jackson, M. I. (eds.), LNCS 207 -- The Analysis of Concurrent Systems, Cambridge, September 1983, Proceedings, Spinger-Verlag (1985), pp. 345--53. There are a number of other contributions by Hoare to the discussions recorded in this volume.Google Scholar
- C. A. R. Hoare and J. He. The weakest prespecification i. Fundamenta Informaticae, 9(1), 51--84 (March 1986).Google Scholar
- C. A. R. Hoare and J. He. The weakest prespecification ii. Fundamenta Informaticae, 9, 217--252 (1986).Google Scholar
- C. A. R. Hoare. The Mathematics of Programming. Oxford University Press (1986). Chapter 21 of the current book.Google Scholar
- A. W. Roscoe and C. A. R. Hoare. Laws of occam Programming. Monograph PRG-53, Oxford University Computing Laboratory, Programming Research Group (February 1986).Google Scholar
- He Jifeng, C. A. R. Hoare, and J. W. Sanders. Data refinement refined: resumé. In Robinet, B. and Wilhelm, R. (eds.), ESOP '86, Springer-Verlag (1986).Google Scholar
- C. A. R. Hoare and He Jifeng. Algebraic specification and proof of properties of a mail service. In Meertens, L. (ed.), IFIP WG 2.1 Working Conference on Program Specification and Transformations, Bad-Tölz, W. Germany 15--17 April, North-Holland Publishers (1986).Google Scholar
- E. R. Olderog and C. A. R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23(1), 9--66 (1986).Google Scholar
- C. A. R. Hoare and He Jifeng. The weakest prespecification. Information Processing Letters, 24(2), 127--32 (January 1987).Google Scholar
- C. A. R. Hoare, He Jifeng, and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2), 71--76, May 1987.Google Scholar
- C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sørensen, J. M. Spivey, and B. A. Sufrin. The laws of programming. Comm. ACM 30(8), 672--87 (August 1987). See Corrigenda in Comm. ACM, 30(9), 770.Google Scholar
- A. I. Enikeev, C. A. R. Hoare, and A. Teruel. [Reference contains text which could not be captured.] Mathematica, 3 (1987) (In Russian)Google Scholar
- He Jifeng and C. A. R. Hoare. Algebraic specification and proof of a distributed recovery algorithm. Distributed Computing, 2(1), 1--12 (1987).Google Scholar
- C. A. R. Hoare and He Jifeng. Design and proof of a mail service. In Friesen, O. and Golshani, F. (eds.), 6th Annual International Phoenix Conference on Computers and Communications -- Conference Proceedings Scottsdale, AZ, USA 25--27 February, 1987, IEEE (1987), pp. 272--5.Google Scholar
- C. A. R. Hoare. An overview of some formal methods for program design. IEEE Computer Journal, 20(9), 85--91 (September 1987). Chapter 22 of the current book.Google Scholar
Cited By
Jones C List of Tony Hoare’s Publications Theories of Programming, (395-410)- Jones C and Misra J Finding Effective Abstractions Theories of Programming, (23-40)
- Kondoh H and Futatsugi K (2006). To use or not to use the goto statement, Science of Computer Programming, 60:1, (82-116), Online publication date: 1-Mar-2006.
- Jones C, Lomet D, Romanovsky A, Weikum G, Fekete A, Gaudel M, Korth H, de Lemos R, Moss E, Rajwar R, Ramamritham K, Randell B and Rodrigues L (2005). The atomic manifesto, ACM SIGOPS Operating Systems Review, 39:2, (41-46), Online publication date: 1-Apr-2005.
- Jones C, Lomet D, Romanovsky A, Weikum G, Fekete A, Gaudel M, Korth H, de Lemos R, Moss E, Rajwar R, Ramamritham K, Randell B and Rodrigues L (2005). The atomic manifesto, ACM SIGMOD Record, 34:1, (63-69), Online publication date: 1-Mar-2005.
- Conn R (2004). A reusable, academic-strength, metrics-based software engineering process for capstone courses and projects, ACM SIGCSE Bulletin, 36:1, (492-496), Online publication date: 1-Mar-2004.
- Conn R A reusable, academic-strength, metrics-based software engineering process for capstone courses and projects Proceedings of the 35th SIGCSE technical symposium on Computer science education, (492-496)
- Bustard D (2001). Software Engineering Books for Desert Island Reading, Automated Software Engineering, 8:1, (121-123), Online publication date: 1-Jan-2001.
- Odersky M (1998). Programming with variable functions, ACM SIGPLAN Notices, 34:1, (105-116), Online publication date: 1-Jan-1999.
- Odersky M Programming with variable functions Proceedings of the third ACM SIGPLAN international conference on Functional programming, (105-116)
- Lederer E and Dumitrescu R Specification-consistent coordination model for computations Proceedings of the 1998 ACM symposium on Applied Computing, (122-129)
- Shavit N, Upfal E and Zemach A A wait-free sorting algorithm Proceedings of the sixteenth annual ACM symposium on Principles of distributed computing, (121-128)
- Wang S (1996). A new sort algorithm, ACM SIGPLAN Notices, 31:3, (28-36), Online publication date: 1-Mar-1996.
- Hansen P Monitors and Concurrent Pascal History of programming languages---II, (121-172)
- Astrachan O and Reed D (1995). AAA and CS 1, ACM SIGCSE Bulletin, 27:1, (1-5), Online publication date: 15-Mar-1995.
- Astrachan O and Reed D AAA and CS 1 Proceedings of the twenty-sixth SIGCSE technical symposium on Computer science education, (1-5)
- Meyer B (1993). Systematic concurrent object-oriented programming, Communications of the ACM, 36:9, (56-80), Online publication date: 1-Sep-1993.
Recommendations
Management Science Roundup
---“MS training in government”;
---“O.R. at a state prison”;
---“Managerial forecasting by 'Super-sophisticated naive' models: Some comments on dent and Swanson's contribution”;
---“News”;
---“Seen Elsewhere: 1 A Cafeteria of Techniques and Critiques by ...
Management Science Roundup
<P>---“NHK-Japan Broadcasting Corporation looks at the 1980S”;</P> <P>---“Fourth Colombian Congress on Operations Research and Computer Sciences”;</P> <P>---“Energy Conservation Study Completed for EPA”;</P> <P>---“Evolution of Operations Research in ...
Martin J. Beckmann-Robert Herman Lifetime Achievement Award in Transportation Science Transportation Science Section Operations Research Society of America April 25, 1994 Boston, Massachusetts
<P>On Monday, April 25, 1994, Martin J. Beckmann was awarded the Robert Herman Lifetime Achievement Award in Transportation Science for his numerous contributions to the field. The award committee consisted of Amedeo Odoni Chairman, David Boyce, Gilbert ...
Hans J. Schneider
This volume contains a selection of C. A. R. Hoare's published papers. Some of them are widely known or even were published on more than one occasion. The original versions of some others cannot be found easily; they are made available to a wider audience only by this book. The papers, selected by C. B. Jones, demonstrate Hoare's contribution to the evolution of methods of reasoning about programs. Twelve of the 22 chapters cover this topic. His work on language definition and his seminal work on parallelism are each seen in about five chapters. Finally, the book includes five papers that are aimed at a wider audience; they concern the role of computer science and especially the importance of formal methods in program construction. The book contains the following papers. :9N(1)The Emperor's Old Clothes (2)Quicksort (3)A Contribution to the Development of ALGOL (See 10, 1 (Jan. 1969), Rev. 15,980.) (4)An Axiomatic Basis for Computer Programming (See 11, 1 (Jan. 1970), Rev. 18,328.) (5)Proof of a Program: Find (See 12, 12 (Dec. 1971), Rev. 22,296.) (6)Procedures and Parameters: An Axiomatic Approach (See 13, 8 (Aug. 1972), Rev. 23,647.) (7)Computer Science (8)Proof of Correctness of Data Representations (9)Proof of a Structured Program: The Sieve of Eratosthenes (10)A Structured Paging System (See 15, 3 (March 1974), Rev. 26,531.) (11)An Axiomatic Definition of the Programming Language Pascal (12)Monitors: An Operating System Structuring Concept (See 16, 4 (Apr. 1975), Rev. 28,126.) (13)Hints on Programming-Language Design (14)Recursive Data Structures (See 16, 11 (Nov. 1975), Rev. 29,165.) (15)Parallel Programming: An Axiomatic Approach (16)Communicating Sequential Processes (17)A Calculus of Total Correctness for Communicating Sequential Processes (See 23, 8 (Aug. 1982), Rev. 39,642.) (18)Programming Is an Engineering Profession (19)A Couple of Novelties in the Propositional Calculus (20)Programs Are Predicates (See Rev. 8602-0132.) (21)The Mathematics of Programming (22)An Overview of Some Formal Methods for Program Design The book starts with Hoare's Turing Award lecture of 1980. All the other papers appear in chronological order of main publication, thus giving a lot of insight into the evolution of our field. The editor supports this insight by adding an introductory remark to each paper, explaining the context in which it was conceived or indicating its influence on subsequent developments. Chapters 7, 21, and 22 provide a good example: they allow the reader to compare the evolution of Hoare's views of how to successfully construct efficient and elegant programs. In 1971, he focused on the requirements; 15 years later, he could offer a solution: “the skills of our best programmers will be even more effective when exercised within the framework of an understanding and application of the relevant mathematical principles.” Another good example is the relative weight given to debugging in chapter 13, which clearly changed as the result of later research. This development manifests itself particularly in the chapters dedicated to methods of reasoning about programs. The paper reproduced as chapter 4 was the most important stimulus to the work on axiomatic semantics. A lot of work started from this seminal paper, which introduced the idea of viewing a program as a predicate transformer. Chapter 5 then presents a thorough proof of the correctness of a particular program, whereas the next chapter considers the impact of this approach on defining new programming languages. In chapter 8, data abstraction is considered to be a key point in developing correct programs. In this chapter as well as in the next, Hoare makes a point of separating the proof of the (more abstract) algorithm from the proof of the concrete data representation. The joint paper with Wirth on the axiomatic definition of Pascal (chapter 11) can be regarded as a summary of how to tackle imperative languages by this approach. Three of the later chapters should also be mentioned in this context. Chapter 14 shows how programming languages can avoid the low-level concept of pointers. (Unfortunately, this paper did not have enough influence on the definition of languages like Ada.) Chapter 19, which is not widely known in the computer science community because it originally appeared in a mathematical publication, presents surprisingly elegant algebraic properties of conditionals. Finally, a new view is proposed in chapter 20, where Hoare no longer treats programs as predicate transformers, but as predicates. This sequence of steps toward program correctness would be incomplete if the book did not include some chapters on parallel processes. Discussion of this topic starts with the paper describing a structured paging system (chapter 10). Chapter 12 reprints Hoare's widely known paper introducing monitors, which not only extended the structured programming approach to process systems but also defined some standard examples that have become test cases for languages as well as for formal methods. These ideas are carried on in chapters 15 and 17, where Hoare proves that processes satisfy assertions on what happens along the channels. Hoare has given many lectures aimed at a wider audience. This volume includes not only his Turing Award lecture, but also his inaugural lectures at both Belfast University (chapter 7) and Oxford University (chapter 21). Chapters 18 and 22 are concerned with examining the engineering component of computer science and, of course, the role of formal methods therein. Moreover, this volume contains one of Hoare's first papers, on the invention of the Quicksort algorithm. It also includes a complete bibliography. Instead of a conclusion, Hoare has added an essay on how to write good papers. It should be put on the reading list of all postgraduate curricula. Hoare was elected to receive the ACM Turing Award “for his fundamental contributions to the definition and design of programming languages. His work is characterized by an unusual combination of insight, originality, elegance, and impact” [1]. The book reflects this; each computer scientist should always have it at hand. The papers have been re-typeset and the references have been made uniform. The book contains only a very small number of misprints. An amusing one is found in the editorial remark introducing chapter 6, where a set of rules is mentioned “which were easy to check statistically” (instead of “statically”).
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.