Theories of Programming: The Life and Works of Tony Hoare
- Length: 450 pages
- Edition: 1
- Language: English
- Publisher: Morgan & Claypool
- Publication Date: 2021-09-26
- ISBN-10: 1450387284
- ISBN-13: 9781450387286
- Sales Rank: #1249645 (See Top 100 Books)
Sir Tony Hoare has had an enormous influence on computer science, from the Quicksort algorithm to the science of software development, concurrency and program verification. His contributions have been widely recognised: He was awarded the ACM’s Turing Award in 1980, the Kyoto Prize from the Inamori Foundation in 2000, and was knighted for “services to education and computer science” by Queen Elizabeth II of England in 2000.
This book presents the essence of his various works–the quest for effective abstractions–both in his own words as well as chapters written by leading experts in the field, including many of his research collaborators. In addition, this volume contains biographical material, his Turing award lecture, the transcript of an interview and some of his seminal papers.
Hoare’s foundational paper “An Axiomatic Basis for Computer Programming”, presented his approach, commonly known as Hoare Logic, for proving the correctness of programs by using logical assertions. Hoare Logic and subsequent developments have formed the basis of a wide variety of software verification efforts. Hoare was instrumental in proposing the Verified Software Initiative, a cooperative international project directed at the scientific challenges of large-scale software verification, encompassing theories, tools and experiments.
Tony Hoare’s contributions to the theory and practice of concurrent software systems are equally impressive. The process algebra called Communicating Sequential Processes (CSP) has been one of the fundamental paradigms, both as a mathematical theory to reason about concurrent computation as well as the basis for the programming language occam. CSP served as a framework for exploring several ideas in denotational semantics such as powerdomains, as well as notions of abstraction and refinement. It is the basis for a series of industrial-strength tools which have been employed in a wide range of applications.
This book also presents Hoare’s work in the last few decades. These works include a rigorous approach to specifications in software engineering practice, including procedural and data abstractions, data refinement, and a modular theory of designs. More recently, he has worked with collaborators to develop Unifying Theories of Programming (UTP). Their goal is to identify the common algebraic theories that lie at the core of sequential, concurrent, reactive and cyber-physical computations.
Theories of Programming Frontispiece Contents Preface Acknowledgements I INTRODUCTION 1 The 1980 ACM Turing Award Lecture 2 Finding Effective Abstractions 2.1 Programming Languages 2.2 Founding the Field of Axiomatic Semantics 2.3 Concurrency 2.3.1 Taming Shared-variable Concurrency 2.3.2 Communicating Processes 2.4 Unifying Theories of Programming A short technical tour References II PROGRAM VERIFICATION 3 Assessing the Success and Impact of Hoare's Logic 3.1 Early Approaches to Program Verification 3.2 Hoare's Logic 3.3 Hoare's Initial Contributions 3.4 Termination 3.5 Influence on Programming Methodology 3.6 Hoare's Reasoning About Recursive Procedures 3.7 Research on Soundness and Completeness 3.8 Reasoning About Arbitrary Procedures 3.9 Parallel Programs 3.10 Distributed Programs 3.11 Object-orientated Programs 3.12 Competing Approaches to Program Verification 3.13 Concluding Remarks Acknowledgements References 4 Preface to Special Issue on Software Verification Acknowledgement 5 The Verified Software Initiative: A Manifesto 5.1 Introduction 5.2 Executive Summary 5.3 Manifesto 5.3.1 Background 5.3.2 Vision 5.3.3 Cost/Benefit 5.3.4 Scientific method and ideals 5.3.5 The scale of collaboration 5.3.6 Industrial participation 5.4 Assessment 5.4.1 Strengths 5.4.2 Weaknesses 5.4.3 Opportunities 5.4.4 Threats 5.5 Conclusions 6 The First Fifteen Years of the Verified Software Project 6.1 Introduction 6.2 The Roots of the Verified Software Initiative 6.3 Theory 6.4 Tools 6.5 Experiments 6.5.1 Competitions 6.5.2 Verified Systems 6.6 The Road Ahead References 7 Verification in the Grand Challenge 7.1 Introduction 7.2 Tokeneer 7.2.1 History of the Development of Tokeneer 7.2.2 The Tokeneer System 7.2.3 Correctness by Construction 7.2.3.1 The Tokeneer Instantiation 7.2.4 The Development Lifecycle 7.2.5 Results of the Tokeneer Experiment 7.2.6 A Personal View (JB) 7.2.7 Influence and Impact 7.3 Research Based on Tokeneer 7.4 Pilot Project: Hypervisor 7.5 What's Next? References III COMMUNICATING SEQUENTIAL PROCESSES 8 Communicating Sequential Processes 8.1 Introduction 8.2 Concepts and Notations 8.2.1 Parallel Commands 8.2.2 Assignment Commands 8.2.3 Input and Output Commands 8.2.4 Alternative and Repetitive Commands 8.3 Coroutines 8.3.1 COPY 8.3.2 SQUASH 8.3.3 DISASSEMBLE 8.3.4 ASSEMBLE 8.3.5 Reformat 8.3.6 Conway's Problem [4] 8.4 Subroutines and Data Representations 8.4.1 Function: Division With Remainder 8.4.2 Recursion: Factorial 8.4.3 Data Representation: Small Set of Integers [11] 8.4.4 Scanning a Set 8.4.5 Recursive Data Representation: Small Set of Integers 8.4.6 Multiple Exits: Remove the Least Member 8.5 Monitors and Scheduling 8.5.1 Bounded Buffer 8.5.2 Integer Semaphore 8.5.3 Dining Philosophers (Problem due to E.W. Dijkstra) 8.6 Miscellaneous 8.6.1 Prime Numbers: The Sieve of Eratosthenes [14] 8.6.2 An Iterative Array: Matrix Multiplication 8.7 Discussion 8.7.1 Notations 8.7.2 Explicit Naming 8.7.3 Port Names 8.7.4 Automatic Buffering 8.7.5 Unbounded Process Activation 8.7.6 Fairness 8.7.7 Functional Coroutines 8.7.8 Output Guards 8.7.9 Restriction: Repetitive Command With Input Guard 8.8 Conclusion Acknowledgement References 9 CSP: A Practical Process Algebra 9.1 Introduction 9.2 Prehistory 1978–1991 9.3 FDR1 1991–1996 : Communication, Fault Tolerance, and the Beginning of Time 9.4 FDR2 1994–2007 at FSEL: Protocols, Abstraction, and Industrial Applications 9.4.1 Translating More Languages into CSP 9.5 FDR2 into Academia: Exploring Implicit Checking and Timed CSP (2007–2012) 9.6 FDR3 and FDR4: Back to Basics and into the Cloud (2012–2019) 9.7 The Future: For CSP and Beyond (2019–) 9.8 Reflections on FDR Acknowledgements References IV TEACHING AND INDUSTRIAL AFFILIATIONS 10 Teaching at Belfast and Oxford 10.1 Introduction 10.2 Queen's University Belfast 10.2.1 Background 10.2.2 Appointment 10.2.3 Taught Degrees 10.2.4 Northern Ireland's ‘Troubles’ 10.2.5 Adieu 10.3 University of Oxford 10.3.1 Background 10.3.2 Appointment 10.3.3 Towards a Viable M.Sc. in Computation 10.3.4 Microprocessors to the Rescue 10.3.5 An Engineering Profession 10.3.6 Breaking the Ice: Towards Undergraduate Degrees 10.3.7 Curriculum Innovation in the Honour School of Mathematics & Computation 10.3.8 A Delayed Inaugural 10.3.9 From Computation to Computer Science: Two New Degrees 10.4 Valediction Acknowledgements References 11 Software Specification 11.1 Precondition–Postcondition Specifications 11.2 Specification of Data Types 11.3 The Role of Specification 11.4 Abstraction in Specification 11.5 Specifying Operations 11.6 Abstract Data Types 11.7 Structuring Specifications Via Aspects 11.8 The IBM/CICS Project 11.9 Industry Influence on Research 11.10 Conclusions References 12 CSP, Occam, and Inmos 12.1 Background 12.2 The Inmos System Language 12.3 Parallel Execution 12.4 Channels 12.5 Alternative 12.6 Timers 12.7 Subroutines 12.8 The Algebraic Specification 12.9 Formal Methods in Hardware Design 12.10 Hardware Design Languages 12.11 General Purpose Parallel Computers 12.12 Impact 12.13 Tomorrow 12.14 Retrospect References V RECENT RESEARCH DIRECTIONS 13 Hoare and He's Unifying Theories of Programming 13.1 Origins of UTP 13.2 Retirement Symposium and UTP Book Launch 13.3 Introduction to UTP 13.4 Relational Calculus 13.5 Relational Semantics of a Programming Language 13.6 Designs 13.7 Galois Connections 13.8 Design Healthiness Conditions 13.9 The UTP School of Semantics References 14 Trimming the Hedges: An Algebra to Tame Concurrency 14.1 Prologue 14.2 Prehistory 14.3 Concurrent Kleene Algebra 14.4 Interchange in Context 14.5 Series-parallel Pomsets, Completeness, and Decidability 14.6 Weak Interchange and Compositional Concurrency 14.7 Other Developments 14.8 Epilogue Acknowledgement References VI RETROSPECT AND PROSPECT 15 Envoi Further resources References VII APPENDICES A ACM Interview B CV B.1 Early Years B.2 Professional Life B.3 Awards and Honours B.4 Other Professional Activities B.5 A Short Photo Album C Doctoral Students D List of Tony Hoare's Publications References E Online Resources Authors' Biographies Index Blank Page
Donate to keep this site alive
1. Disable the AdBlock plugin. Otherwise, you may not get any links.
2. Solve the CAPTCHA.
3. Click download link.
4. Lead to download server to download.
