Tag Archives: Hoare 邏輯

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

為什麼這麼慢呢?Bentley 和 McIlroy 認為問題出在我們花了太多工夫把兩個白色元素一步步挪到中間。與其如此,不如先把白色元素放到兩邊去,把陣列排成「白、紅、藍、白」。等排序完成,再把白色換回中間就可以了!

Posted in 計算算計 | Also tagged | Leave a comment

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

這是一個 O(N-M) 的程式。如果三色數量相同,我們平均需要大約 2(N-M)/3 次交換。如果我們當初選擇從檢查 a[b-1] 開始,平均需要的交換次數則是 N-M 次。

Posted in 計算算計 | Also tagged | Leave a comment

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

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

Posted in 計算算計 | Also tagged , | 4 Comments

距離平方和

給定一個有兩個以上元素的陣列a, 計算任兩個元素前者減後者所得之差的平方的總和。

Posted in 計算算計 | Also tagged , | 3 Comments

再看二元搜尋法 Binary Search(下)

給定一個排序好的陣列 a[0..N)(其元素為 a[0], a[1]a[N-1]), 0 ≤ N。如何用 van Gasteren 與 Feijen 的方法判斷其中是否含有某個關鍵值 K 呢?

Posted in 計算算計 | Also tagged | 1 Comment

再看二元搜尋法 Binary Search(上)

如果你自認對二元搜尋 (binary search) 夠熟悉了,卻沒讀過 Netty van Gasteren 和 Wim Feijen 的研究筆記 The Binary Search Revisited, 強烈建議你找時間看看。

Posted in 計算算計 | Also tagged | 3 Comments

程式設計的公設基礎:四十年後

1969 年,C.A.R. Hoare 在 Communication of the ACM (12(10):576–580) 發表論文 An Axiomatic Basis for Computer Programming,在文中提出後來被稱作 Hoare 邏輯的一套公設系統, 被認為是計算科學史上最重要的幾篇論文之一。時間轉眼間過去了,今年已經是這篇論文的四十歲生日。

Posted in 人物, 計算算計 | Also tagged , , | 2 Comments