Theories of programming : the life and works of Tony Hoare / Cliff B. Jones, Jayadev Misra [editors].

Format:

Book

Contributor:

Misra, Jayadev.

Jones, C. B. (Cliff B.), 1944- editor.

Misra, Jayadev, editor.

Series:

ACM books ; #39.

ACM books, 2374-6777 ; #39

Language:

English

Subjects (All):

Hoare, C. A. R. (Charles Antony Richard), 1934-.

Hoare, C. A. R.

Computer programming.

Software engineering.

Programming languages (Electronic computers).

Theories of Programming (Computer Programming).

computer programming.

Local Subjects:

Theories of Programming (Computer Programming).

Physical Description:

1 online resource (452 pages)

Edition:

1st ed.

Other Title:

Theories of Programming

Place of Publication:

San Rafael : Morgan & Claypool Publishers, 2021.

Summary:

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.

Contents:

Intro

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

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

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?

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

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

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 &amp

Computation

10.3.8 A Delayed Inaugural

10.3.9 From Computation to Computer Science: Two New Degrees

10.4 Valediction

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

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

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

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

VI RETROSPECT AND PROSPECT

15 Envoi

Further resources

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

E Online Resources

Authors' Biographies

Index

Blank Page.

Notes:

Description based on publisher supplied metadata and other sources.

ISBN:

9781450387316

1450387314

OCLC:

1321802290