標籤
λ calculus 二元搜尋法 函數編程 單子 型別 抽象資料型別 模型檢查 歷史 河內塔問題 演算法 物件導向 程式推導 結構化程式 資料抽象化 資料結構 邏輯 Aad van Wijngaarden Alan Turing ALGOL Benjamin Pierce Christopher Strachey Colossus Coq Dan Piponi Edsger Dijkstra Erik Meijer FLOLAC Guy Steele Haskell Hoare 邏輯 ICFP Jaap Zonneveld Jean-Pierre Jouannaud Luca Cardelli Mervyn Pragnell Oleg Kiselyov Peter J. Landin Peter Naur Peter Wegner Ralf Hinze Rod Burstall SCI Turing 機器 Turing 測試 William Cook分類
-
最近文章
-
最近回應
彙整
Tag Archives: Hoare 邏輯
再看二元搜尋法 Binary Search（上）
如果你自認對二元搜尋 (binary search) 夠熟悉了，卻沒讀過 Netty van Gasteren 和 Wim Feijen 的研究筆記 The Binary Search Revisited, 強烈建議你找時間看看。
程式設計的公設基礎：四十年後
1969 年，C.A.R. Hoare 在 Communication of the ACM (12(10):576–580) 發表論文 An Axiomatic Basis for Computer Programming，在文中提出後來被稱作 Hoare 邏輯的一套公設系統, 被認為是計算科學史上最重要的幾篇論文之一。時間轉眼間過去了，今年已經是這篇論文的四十歲生日。
再看二元搜尋法 Binary Search（下）
a[0..N)（其元素為a[0],a[1]...a[N-1]）,0 ≤ N。如何用 van Gasteren 與 Feijen 的方法判斷其中是否含有某個關鍵值K呢？