Edsger Wybe Dijkstra : His Life, Work, and Legacy / Krzysztof R. Apt and Tony Hoare (editors).

Format:

Book

Contributor:

Apt, Krzysztof R., 1949- editor.

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

Series:

ACM books.

ACM Books

Language:

English

Subjects (All):

Computer programmers--Biography.

Computer programmers.

Computer programming.

Dijkstra, Edsger W.

Physical Description:

1 online resource (574 p.)

Edition:

First edition.

Place of Publication:

[Place of publication not identified] : Association for Computing Machinery, [2022]

Summary:

Edsger Wybe Dijkstra (1930-2002) was one of the most influential researchers in the history of computer science, making fundamental contributions to both the theory and practice of computing. Early in his career, he proposed the single-source shortest path algorithm, now commonly referred to as Dijkstra's algorithm. He wrote (with Jaap Zonneveld) the first ALGOL 60 compiler, and designed and implemented with his colleagues the influential THE operating system. Dijkstra invented the field of concurrent algorithms, with concepts such as mutual exclusion, deadlock detection, and synchronization. A prolific writer and forceful proponent of the concept of structured programming, he convincingly argued against the use of the Go To statement. In 1972 he was awarded the ACM Turing Award for "fundamental contributions to programming as a high, intellectual challenge; for eloquent insistence and practical demonstration that programs should be composed correctly, not just debugged into correctness; for illuminating perception of problems at the foundations of program design." Subsequently he invented the concept of self-stabilization relevant to fault-tolerant computing. He also devised an elegant language for nondeterministic programming and its weakest precondition semantics, featured in his influential 1976 book A Discipline of Programming in which he advocated the development of programs in concert with their correctness proofs. In the later stages of his life, he devoted much attention to the development and presentation of mathematical proofs, providing further support to his long-held view that the programming process should be viewed as a mathematical activity.In this unique new book, 31 computer scientists, including five recipients of the Turing Award, present and discuss Dijkstra's numerous contributions to computing science and assess their impact. Several authors knew Dijkstra as a friend, teacher, lecturer, or colleague. Their biographical essays and tributes provide a fascinating multi-author picture of Dijkstra, from the early days of his career up to the end of his life.

Contents:

Intro

Edsger Wybe Dijkstra

Contents

Preface

Photo Credits

Photos

I INTRODUCTION

1 The Humble Programmer

II TECHNICAL PERSPECTIVES ON DIJKSTRA'S WORK

2 Dijkstra's Single Source Shortest Path Algorithm

2.1 Dijkstra's Algorithm

2.2 Implementations

2.2.1 Integer Weights

2.3 Dijkstra's SSSP and Beyond

Acknowledgment

References

3 Programming Concurrent Systems

Abstract

3.1 Introduction

3.2 Concurrency

3.2.1 Language Constructs for Concurrency

3.3 Why Concurrency?

3.4 Atomicity and Commuting

3.5 Taxonomy of Concurrency: Shard, Stream, or Struggle

3.6 Sharding

3.7 Streaming

3.8 Easy Concurrency

3.8.1 Monitors

3.8.2 Scheduling

3.9 Hard Concurrency

3.9.1 Multiple Versions and Wait-free Concurrency

3.10 Eventual Consistency

3.11 Nuisance Concurrency

3.12 Conclusion

4 Concurrent Algorithms

4.1 Introduction

4.2 Mutual Exclusion

4.2.1 Preliminaries

4.2.2 Dekker's Algorithm

4.2.3 Dijkstra's Algorithm

4.2.4 Semaphores

4.2.5 A Closer Look at the Problem

4.2.6 The Dining Philosophers

4.3 Self-stabilization

4.3.1 The Problem

4.3.2 A Coarse-grained Algorithm

4.3.3 A Finer-grained Algorithm

4.3.4 What Dijkstra Actually Wrote

4.3.5 The Paper's Influence

4.4 On-the-fly Garbage Collection

4.4.1 The Problem

4.4.2 A Solution

4.4.3 Verification

4.4.4 The Algorithm and its Significance

4.5 Termination Detection

4.5.1 The Problem

4.5.2 The Tree Algorithm

4.5.3 The Ring Algorithm

4.5.4 A Bit of History

4.6 Conclusion

5 Origin of Self-Stabilization

5.1 Introduction

5.2 Privileges in a Ring

5.3 Privileges in an Array

5.4 Distance Convergence on a Circle

5.5 Complexity and Verification

5.6 Relevance

5.7 Adoption

5.8 Impact

5.8.1 Possibility.

5.8.2 Applications

5.8.3 Complexity

5.8.4 Atomicity

5.8.5 Schedulers

5.8.6 Model Exploration

5.8.7 Fault-tolerance

5.9 Conclusions

6 Dijkstra's Legacy on Program Verification

6.1 Dijkstra's View of Program Verification

6.1.1 A Posteriori Verification versus Correctness-by-Construction

6.1.2 Criticism

6.1.3 Informal, Rigorous, Formal, Mechanized, Automated

6.2 The Weakest Precondition Calculus and Its Context

6.2.1 Setting the Stage

6.2.2 Floyd and Hoare

6.2.3 Guarded Commands

6.2.4 The Weakest Precondition Calculus

6.2.5 Symbolic Execution

6.2.6 Relational Calculus

6.2.7 Dynamic Logic

6.3 From Program Correctness to Program Certification

6.3.1 Understanding and "Understanding"

6.3.2 Program Verification at Scale

6.3.3 The VCG Architecture

6.3.4 Going Backwards by Forward Reasoning

6.4 The Future of the Legacy

6.4.1 Weakest Precondition Reasoning

6.4.2 Theory and Practice of Program Verification

6.4.3 phv and cbc Revisited

6.4.4 Towards a New Discipline

7 Development of Correct Programs

7.1 Recurring Themes

7.2 What's a Proof?

7.2.1 Divide and Conquer

7.2.2 Three Mental Aids

7.3 Structured Programming, with Proof of Correctness the Main Concern

7.4 1968 NATO Conference on Software Engineering

7.5 1968-1969: A Period of Suffering

7.6 The Development of Weakest Preconditions

7.7 A Calculus Based on Leibniz's Substitution of Equals for Equals

The Everywhere Operator

7.8 Proofs of Concurrent Programs

7.9 Conclusion

8 Nondeterminism and Guarded Commands

8.1 Introduction

8.2 Avoiding Nondeterminism

8.2.1 Grammars

8.2.2 Abstract Reduction Systems

8.3 Angelic Nondeterminism

8.3.1 Nondeterministic Finite Automata and Turing Machines.

8.3.2 McCarthy's Ambiguity Operator

8.3.3 Floyd's Approach to Nondeterministic Programming

8.3.4 Logic Programming and Prolog

8.3.5 Does Angelic Nondeterminism Add Expressive Power?

8.4 Guarded Commands

8.5 Some Considerations on Guarded Commands

8.6 Modeling Parallel Programs

8.7 Communicating Sequential Processes and Their Relation to Guarded Commands

8.8 Fairness

8.9 Nondeterminism: Further Developments

8.9.1 Taxonomy of Nondeterminism

8.9.2 Nondeterminism in a Context

8.10 Conclusions

Acknowledgements

9 A Personal View of Edsger W. Dijkstra and His Stance on Software Construction

10 Applying Dijkstra's Vision to Numerical Software

10.1 Introduction

10.2 An Example

10.2.1 The Goal

10.2.2 Notation, Notation, Notation

10.2.3 Deriving Algorithms

10.2.4 Representing Algorithms in Code

10.3 Decades of Research, Development, and Impact

10.3.1 Parallel Computing: Driving a Desperate Need for Simplicity

10.3.2 Notation, Again

10.3.3 FLAME

10.3.4 Turning Knowledge into a System

10.3.5 Making a System Mechanical

10.3.6 Correctness in the Presence of Round-off Error

10.3.7 Sidestepping the Phase Ordering Problem

10.3.8 Beyond Dense Linear Algebra

10.3.9 Turning Theory into Practice: Libflame

10.4 Educating the Masses

10.5 Conclusion

Acknowledgments

11 Calculational Proofs

11.1 A letter from Dijkstra

11.2 Dijkstra's Calculational Proofs are Semi-formal

11.3 Calculational Proofs Can Be Smooth

11.4 Calculational Proofs versus Natural Deduction

11.5 Propositional Calculations

11.6 Reasoning about Predicate Transformers

11.7 Conclusion

12 An Homage to the Beautiful Mathematical EWDs

12.1 Kruskal's Algorithm for Minimum Spanning Tree.

12.1.1 Minimum Spanning Tree, Kruskal's Algorithm

12.1.2 Dijkstra's Lemma

12.1.3 Proof of Kruskal's Algorithm

12.1.4 Dijkstra-Prim Minimum Spanning Tree Algorithm

12.1.5 A Critique of EWD1273

12.2 Fermat's and Wilson's Theorems

12.2.1 Fermat's Little Theorem

12.2.2 Wilson's Theorem

12.2.3 A Critique of EWD742

12.3 Arithmetic and Geometric Mean

12.3.1 Dikstra's Proof of the am-gm Inequality

12.3.2 A Critique of EWD1171

12.4 Hall's Theorem on Distinct Representatives

12.4.1 Distinct Representatives

12.4.2 A Proof of Hall's Theorem

12.4.3 A Simpler Proof of Hall's Theorem

12.5 Coxeter's Rabbit

12.5.1 A Critique of EWD1318

12.6 Concluding Remarks

Acknowledgement

III SELECTED PAPERS

13 A Note on Two Problems in Connexion with Graphs

14 Recursive Programming

14.1 The Aim

14.2 The Stack

14.3 Stacked Reservations

14.4 Consequences

14.5 The Link

14.6 Recursive Techniques and ALGOL 60

Reference

15 Some Meditations on Advanced Programming

16 Solution of a Problem in Concurrent Programming Control

Introduction

The Problem

The Solution

The Proof

17 Go To Statement Considered Harmful

Key Words and Phrases

CR Categories

18 The Structure of the "THE"-Multiprogramming System

KEY WORDS AND PHRASES

CR CATEGORIES

18.1 Introduction

18.2 The Tool and the Goal

18.3 A Progress Report

18.4 A Survey of the System Structure

18.5 Design Experience

18.6 Conclusion

18.A Appendix

18.A.1 Synchronizing Primitives

18.A.2 Mutual Exclusion

18.A.3 Private Semaphores

18.A.4 Proving the Harmonious Cooperation

19 Self-stabilizing Systems in Spite of Distributed Control

Solution with K-state Machines (K &gt.

N)

Solution with Four-state Machines

Solution with Three-state Machines

20 On-the-Fly Garbage Collection: An Exercise in Cooperation

20.1 Introduction

20.2 The Grain of Action

20.3 Reformulation of the Problem

20.4 The First Coarse-Grained Solution

20.5 A New Coarse-Grained Solution

20.6 A Fine-Grained Solution

20.6.1 In Retrospect

20.6.2 Glossary of Names

21 On the Reliability of Programs

IV BIOGRAPHICAL ESSAYS

22 Edsger Dijkstra, The Man Who Carried Computer Science on His Shoulders

22.1 Biography

22.2 EWDs

22.3 Early Contributions

22.4 Eighties

22.5 Nineties

22.6 Opinions and Attitudes

22.7 Character and Lifestyle

22.8 Legacy

23 Memories of Edsger W. Dijkstra

23.1 Weakest Preconditions

23.2 Fairness

23.3 Personal Reminiscences

24 Reflections on Edsger and His Influence

25 Forty Years with Edsger

26 Edsger Dijkstra-Some Reminiscences

26.1 Introduction

26.2 Brighton 1961

26.3 Visit to the Mathematical Centre

26.4 Our Trip Report and Book

26.5 1964-IBM and Algol WG 2.1

26.6 1967-SOSP

26.7 The THE Operating System

26.8 The 1968 NATO S/W Engineering Conference

26.9 Algol 68

26.10 The 1969 NATO Conference

26.11 In 12 Months from June 1974

26.12 Some EWD Interludes

26.13 The 60th Birthday Salute

27 Evoking Whitehead's Dictum

27.1 Dijkstra's Influence: On Concurrent Programming

27.2 Dijkstra's Influence: On Becoming a Researcher

28 Edsger W. Dijkstra in the Eyes of His Friends, Colleagues, and Students

28.1 Lex Bijlsma, Open University of the Netherlands

28.2 Ken Calvert, University of Kentucky, Lexington, KY.

28.3 K. Mani Chandy, California Institute of Technology, Pasadena, CA.

Notes:

Description based on publisher supplied metadata and other sources.

Description based on print version record.

Includes bibliographical references and index.

ISBN:

9781450397742

1450397743