More than anything else, this book is a tribute to Edsger W. Dijkstra, on the occasion of his sixtieth birthday, by just a few of those fortunate enough to be influenced by him and his work and to be called his friend or relation, his master, colleague, or pupil. This book contains fifty-four technical contributions in different areas of endeavor, although many of them deal with an area of particular concern to Dijkstra: programming. Each contribution is relatively short and could be digested in one sitting. Together, they form a nice cross section of the discipline of programming at the beginning of the nineties. While many know of Dijkstra's technical contributions, they may not be aware of his ultimate goal, the mastery of complexity in mathematics and computing science. He has forcefully argued that beauty and elegance are essential to this mastery. The title of this book, chosen to reflect his ultimate goal, comes from a sentence in an article of his on some beautiful arguments using mathematical induction: "... when we recognize the battle against chaos, mess, and unmastered complexity as one of computing sci- ence's major callings, we must admit that 'Beauty Is Our Business'."
Author(s): W.H.J.Feijen, A.J.M. van Gasteren, D.Gries, J.Misra (eds.)
Series: Texts and Monographs in Computer Science
Publisher: Springer
Year: 1990
Language: English
Pages: 473
Tags: Programming Techniques; Logics and Meanings of Programs; Mathematical Logic and Formal Languages
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
