Theories of Programming / The Life and Works of Tony Hoare / Cliff B. Jones, Jayadev Misra.

Format:

Book

Author/Creator:

Jones, Cliff B., editor.

Series:

ACM books - Collection 2 ; #39.

ACM books, 2374-6777 ; #39

Language:

English

Subjects (All):

Theories of Programming (Computer Programming).

Genre:

Electronic books.

Physical Description:

1 online resource (xx, 430 pages) LuaTEX

Edition:

First Edition

Place of Publication:

[New York, NY, USA] : Association for Computing Machinery; [2021].

System Details:

Mode of access: World Wide Web

System requirements: Adobe Acrobat Reader

Contents:

Preface

PART 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.4 Unifying Theories of Programming

References

PART 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

5 The Verified Software Initiative: A Manifesto

5.1 Introduction

5.2 Executive Summary

5.3 Manifesto

5.4 Assessment

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.6 The Road Ahead

7 Verification in the Grand Challenge

7.1 Introduction

7.2 Tokeneer

7.3 Research Based on Tokeneer

7.4 Pilot Project: Hypervisor

7.5 What's Next?

PART III COMMUNICATING SEQUENTIAL PROCESSES

8 Communicating Sequential Processes

8.1 Introduction

8.2 Concepts and Notations

8.3 Coroutines

8.4 Subroutines and Data Representations

8.5 Monitors and Scheduling

8.6 Miscellaneous

8.7 Discussion

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.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.8 The Future: For CSP and Beyond (2019-)

9.9 Reflections on FDR

PART IV TEACHING AND INDUSTRIAL AFFILIATIONS

10 Teaching at Belfast and Oxford

10.1 Introduction

10.2 Queen's University Belfast

10.3 University of Oxford

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

PART 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

PART VI RETROSPECT AND PROSPECT

15 Envoi

PART VII APPENDICES

Appendix A ACM Interview

Appendix 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

Appendix C Doctoral Students

Appendix D List of Tony Hoare's Publications

Appendix E Online Resources

Author's Biographies

Index

Other Format:

Print version:

ISBN:

3477355

9781450387316

9781450387309

Access Restriction:

Restricted for use by site license.