Edsger Dijkstra

除二、相減,大小不變?來自《結構化編程》中的一個小例子

請問如何論證:如果 0 ≤ r < dd 成立,經過這兩行程式後,0 ≤ r < dd 仍成立?

dd := dd / 2;
if dd ≤ r then r := r - dd

這個例子來自 Dahl, Dijkstra & Hoare 1972 年的 Structured Programming. 書名引起我的注意:「結構化程式設計」在 70, 80 年代曾被學界、業界視為軟體危機的解方、所有人寫程式該遵守的圭臬。但每個陣營對它是什麼都各有一套解釋。數十年過去,structured programming 卻以一種不知能否算功成而退的方式被遺忘:現在的學生們自然地把程式寫成塊狀的結構,許多人甚至已經不知有 goto 這個指令。但他們沒聽過 structured programming, 對於 Dijkstra 等人當年提倡的程式推論仍一樣地陌生。

我想知道這套概念的創始者們怎麼談它,因此好奇地想讀這本書。

「讓程式能依據其結構被理解、被證明」便是我心目中的「結構化編程」。而在那個時代,他們的挑戰便是設計語言、符號,使得這種編程與推論成為可能。

荷蘭國旗問題 The Dutch National Flag Problem(上)

陣列裡頭每個元素都是紅、白、藍三色之一。如何把它們由左至右依紅、白、藍的順序排好呢?Dijkstra 希望採用三向分割法後能更容易表達紅(小於 pivot)和藍色(大於 pivot)的區塊絕對比原陣列短的性質。然而,在 Peter 的印象中 Dijkstra 從沒把這層考量寫下來。「我們如果不告訴學生,以後就沒人知道了呢!」他說。