Beauty Is Our Business: A Birthday Salute to Edsger W. Dijkstra

Front Matter....Pages i-xix
Proving Termination of Parallel Programs....Pages 1-6
On a Relation on Functions....Pages 7-18
Efficient Solution of a Non-Monotonic Inverse Problem....Pages 19-26
Semantics of Quasi-Boolean Expressions....Pages 27-35
Small Specification Exercises....Pages 36-43
Architecture of Real-Time Systems....Pages 44-53
The Use of a Formal Simulator to Verify a Simple Real Time Control Program....Pages 54-66
Exploring the Future: Trends and Discontinuities....Pages 67-75
On a Renewed Visit to the Banker and a Remarkable Analogy....Pages 76-82
On Bounded Buffers: Modularity, Robustness, and Reliability in Reactive Systems....Pages 83-93
Examples in Program Composition....Pages 94-101
On the Mechanism of the Hydrogenation of Edible Oils....Pages 102-111
The Problem of the Majority Network....Pages 112-118
A Little Exercise in Deriving Multiprograms....Pages 119-126
Experimenting with a Refinement Calculus....Pages 127-134
Serializable Programs, Parallelizable Assertions: A Basis for Interleaving....Pages 135-140
Binary to Decimal, One More Time....Pages 141-148
Rotate and Double....Pages 149-162
Beautifying Gödel....Pages 163-172
A Striptease of Entropy....Pages 173-175
On a Theorem of Jacobson....Pages 176-181
Modalities of Nondeterminacy....Pages 182-192
A Theory for the Derivation of C-mos Circuit Designs....Pages 193-205
On Mathematical Induction and the Invariance Theorem....Pages 206-211
Formalizing Some Classic Synchronization Primitives....Pages 212-219
Consequences....Pages 220-225
Shortest and Longest Segments....Pages 226-232
A Simple Program Whose Proof Isn’t....Pages 233-242
Binding Structure and Behaviour in “Whole Net” Concurrency Semantics....Pages 243-250
Maximal Strong Components: An Exercise in Program Presentation....Pages 251-261
A Systolic Program for Gauss-Jordan Elimination....Pages 262-273
Coding for Channels with Localized Errors....Pages 274-279
Topology-Independent Algorithms Based on Spanning Trees....Pages 280-288
An Exercise in the Verification of Multi-Process Programs....Pages 289-301
The Limitations to Delay-Insensitivity in Asynchronous Circuits....Pages 302-311
A Simple Proof of a Simple Consensus Algorithm....Pages 312-318
Of wp and CSP....Pages 319-326
Programming by Expression Refinement: the KMP Algorithm....Pages 327-338
Methodical Competitive Snoopy-Caching....Pages 339-345
Beauty and the Beast of Software Complexity — Elegance versus Elephants....Pages 346-351
A Note on Feasibility....Pages 352-355
A Curious Property of Points and Circles in the Plane....Pages 356-357
A Problem Involving Subsequences....Pages 358-364
A Personal Perspective of the Alpern-Schneider Characterization of Safety and Liveness....Pages 365-372
Simpler Proofs for Concurrent Reading and Writing....Pages 373-379
Goodbye Junctivity?....Pages 380-385
An Assignment Problem for the Vertices of a Cycle....Pages 386-389
Duality and De Morgan Principles for Lists....Pages 390-398
The Quest for Timeless Specifications Leads to Non-Stepping Automata....Pages 399-409
The Maximum Length of a Palindrome in a Sequence....Pages 410-416
On Form, Formalism and Equivalence....Pages 417-426
Drawing Lines, Circles, and Ellipses in a Raster....Pages 427-434
Calculations with Relations, an Example....Pages 435-441
Two Proofs for Pythagoras....Pages 442-447
Back Matter....Pages 448-453