Hoare 邏輯

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

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