基本介紹
編輯推薦本書寫於20世紀70年代中後期，但其對編程技術領域的開發、程式語言發展和程式理論研究有深刻影響。
內容提要
本書是圖靈獎獲得者Edsger W. Dijkstra在編程領域裡的經典著作中的經典。作者基於其敏銳的洞察力和長期的實際編程經驗，對基本順序程式的描述和開發中的許多關鍵問題做了獨到的總結和開發。書中討論了順序程式的本質特徵、程式描述和對程式行為（正確性）的推理，並通過一系列從簡單到複雜的程式的思考和開發範例，闡釋了基於嚴格的邏輯推理開發正確可靠程式的過程。本書值得每個關注計算機科學技術的本質，冀求在程式和軟體領域有長遠發展的計算機工作者、教師和學生閱讀。
書本目錄
序 IX前言 XI
第0章執行抽象 1
第1章程式語言的作用 13
第2章狀態及其特徵 19
第3章語義的性質 29
第4章一種程式語言的語義特徵 47
第5章兩個定理 73
第6章論完滿終止結構的設計 81
第7章再論歐幾里得算法 89
第8章幾個小例子的形式化處理 101
第9章論受限的非確定性 143
第10章有關記法的短論：“變數的作用域” 157
第11章數組變數 187
第12章線性檢索定理 209
第13章下一個排列 213
第14章荷蘭國旗問題 221
第15章更新順序檔案 233
第16章再論歸併 245
第17章來自R。W。HAMMING的一個練習 257
第18章模式匹配問題 269
第19章將一個數寫成兩個平方之和 279
第20章大數的最小素因子問題 285
第21章最孤立村莊問題 297
第22章最短子支撐樹問題 307
第23章記錄等價類的REM算法 321
第24章三維空間的凸包問題 335
第25章有向圖的最大強連通分支 383
第26章論手冊和實現 401
第27章跋 417
精彩節摘
序在詩歌、音樂、藝術和科學等歷史更為悠久的智力修煉領域，歷史學家們都把頌詞獻給那裡最卓越的實踐者，因為他們的成就拓展了其讚美者的體驗和理解，也大大啟迪和提升了其追隨者們的才華。他們的創新基於其在實踐中積累的卓越技藝，並結合了他們對相應領域的基礎理論的敏銳洞見。在很多情況下，他們的影響還由於其廣博的文化積澱，以及他們在表達方式上的力量和透徹性而得到進一步的提升。
C.A.R.Hoare
作者簡介
作者介紹
艾茲赫爾·戴克斯特拉（Edsger W. Dijkstra，1930年5月11日－2002年8月6日），生於荷蘭鹿特丹，自喻為荷蘭第一個以程式設計作為職業的人。他早年積極推動結構化程式設計，一生致力於將計算（computing）發展為一門科學，在計算機科學技術的諸多領域有開拓性建樹，並由於在程式設計基礎研究中的卓越貢獻獲得1972年圖靈獎。譯者介紹
裘宗燕，北京大學數學學院教授。主要研究興趣是軟體形式化方法和程式設計的理論基礎，也關注程式設計實踐。翻譯過若干相關著作，包括《從規範出發的程式設計》、《B方法》、《編程原本》、《電腦程式的構造和解釋》、《C++語言的設計和演化》等。媒體評論
在本書中，作者以其習慣的文字風格，詳盡地描述了他對計算機編程的基本性質的激進的新見解。基於這些見解，作者開發了一套編程方法以及與之相適應的記法工具，並用一大批優雅而且高效的實例展示和檢驗了它們。本書將注定成為在計算機編程的智力修煉領域發展中最傑出的成就之一。C.A.R.Hoare
前言
很長時間以來，我一直想寫一本基本上是按照本書線索的著作，原因是：一方面，我知道程式可以有迷人的形態和深刻的邏輯之美；另一方面，我又不得不接受這樣的事實，即絕大部分程式只是以一種適合機器執行的方式表達，完全沒有什麼美感，也不適合人們欣賞。這種不滿意還有第二個原因，那就是各種算法通常總是以一種完成了的產品形式發表，而在設計過程中起著最重要作用的，以及成為證明所完成程式的最終形式的正當性的各種思考的主要部分，通常都完全沒有提及。我最初的想法是以讀者能欣賞到它們的美的方式發表一系列優美的算法。對於如何做這件事，我當時的想法是描述一些實際的和想像中的設計過程，使其中的每個過程最終都得到了一個所需的程式。我在一定程度上實現了最初的想法，作為這本專著的核心部分是一系列的章節，每一章處理並解決一個新問題。而在另一方面，最終寫出的這本書與我早前的期望又有很大不同，由於我特別希望用一種自然而且方便的方式來展現這些內容，因這種追求而強加給自己的任務變成了一種重要的責任。我將永遠為自己完成了這一工作而感到欣慰。在開始寫一本像本書這樣的著作時，人們立刻會面臨一個問題：“我準備使用哪一種程式語言？”而實際上這並不僅僅是一個有關展示形式的問題！任何工具的一個最重要的（而且也是最難琢磨的）方面，就是它對於被訓練而將使用它的人們的工作習慣的影響，這種影響——無論我們是否喜歡——是對我們的思考習慣的影響。在儘可能地分析了這種影響的各方面情況之後，我得出了一個結論：沒有一個現存的語言，也沒有一個它們的子集適合我的目標。其次，我也知道自
己完全沒有為設計一種新的程式語言做好準備，因此，我曾發誓在隨後的五年里不去做這件事。而且我有一種非常清晰的感覺：這個時期還沒有過去！（但還有一個前提，就是除了其他事情外，這本書必須要寫。）我試著消解這一矛盾的方式是設計了一個適合我的具體目標的小型語言，只做出一些看起來不可能避免，而且其正當性也得到了充分證實的承諾。
這種猶豫和自我強加的約束如果被錯誤地理解，有可能使本書的許多潛在讀者對它感到很失望。那些把編程的困難等同於老練地利用那些精細而花哨的稱為“高級程式語言”的工具，或者（更糟糕的！）“編程系統”的困難的人們注定會對這本書不滿意。如果因為我忽略了所有那些誘人的花哨玩意兒而使他們感到受了騙，我只能回答說：“你真能確定所有那些誘人的花哨玩意兒，以及那些你所謂‘強大的’程式語言的美妙功能確實屬於解集合，而不屬於問題的集合嗎？”我只是希望，即便我用的是一種小型語言，他們也能看看這本書。在做完這件事之後，他們有可能同意，雖然沒有那些誘人的花哨玩意兒，仍然有非常豐富的問題需要討論。因此，是否在一開始就介紹大部分花哨玩意兒，確實是應該質疑的。還有，對於那些明顯是對程式語言的設計有興趣的讀者，我只能表示我的歉意。正如我已經做的那樣，我沒辦法在這個問題上做更明確的事情。但在另一方面，我也希望隨著時間的推移，這一專著會對他們有所啟示，而且能幫助他們避免一些如果沒有讀過它有可能犯的錯誤。
在寫作的過程中——它持續不斷地讓我感到驚喜和激動——逐漸呈現的文本與我初始時頭腦中的想像大不相同。我一開始構想以一種（易理解的）方式去展示程式的開發過程，帶上比我在（引論）課程中更多一點的形式化設施，其中以直觀的方式介紹所使用的語義，有關正確性的論證採用通常的嚴格論述，手工編排，再加上有說服力的文字。在為更形式化的方法建立了必要的基礎後，我得到了兩個驚喜。第一個驚喜就是所謂的“謂詞轉換器”，作為我選用的工具，它提供了一種方法，使我們可以直接定義初始狀態與最終狀態之間的關係，不需要參考在程式實際執行中可能經歷的中間狀態。我對這種情況感到非常欣慰，因為這清晰地區分了程式設計師的兩個主要關注點：數學的正確性（即程式是否定義了初始狀態與最終狀態之間所需的正確關係——謂詞轉換器是我們研究這一問題的一種形式化工具，研究中不需要考慮實際的計算進程），以及工程上對於效率的關注。這已經成為一種最有幫助的發現，因為同一個程式正文總是有兩種相當互補的解釋：它可以解釋為一個謂詞轉換器的編碼，這樣做看起來更適合我們的需要；或者解釋為可執行代碼，我寧願把這種解釋留給機器去做。第二個驚喜是，我能夠想像到的最自然而且最系統化的“謂詞轉換器的編碼”，在被看作“可執行代碼”時，將要求一種非確定性的實現。有一段時間，我對把非確定性引進單道編程感到不寒而慄（我對它給多道編程帶來的複雜性知道得太多了！），直到我認識到，將程式正文解釋為一個謂詞轉換器的編碼有其自身的存在理由。（回顧往事，我們可以看到，過去提出的有關多道編程的許多問題並不是別的什麼，只不過是不適當地過分強調了確定性的重要性而帶來的後果。）我最終認識到，應該把非確定性看作正常情況，這樣，確定性將變成一種——並不很有趣的——特例了。
在打好了有關的基礎之後，我將所有的時間都投入了想做的事情上，也就是說，去解決一系列的問題。做這件事使我得到了未曾預料的快樂。與我以前的工作方式相比，形式化的設施使我能更牢固地把握所做的工作。我很高興地發現，明確地關注終止性問題能帶來許多富於啟發性的看法，以至於使我覺得偏向於考慮部分正確性的觀點如此常見是非常令人遺憾的。然而，最大的快樂是，對於大部分我原來做過的問題，這次都得到了更漂亮的解答！這是非常令人鼓舞的事情，我將它看作是一種指示劑，說明我所開發的方法確實提升了我的編程能力。
應該怎樣學習這本專著呢？我能給出的最佳建議就是，一旦看完了問題的描述，就停止閱讀，轉去試著自己解決它。嘗試自己解決問題，是你能自己認識和評價問題的困難程度的唯一方法，它也使你有機會去比較你的解和我給出的解，還給你得到滿足的機會，即看到你給出的解比我給出的更好。還是要先說一下，當你發現這裡的內容遠不是非常容易讀的時候，請不要沮喪。研讀過這本專著的人都覺得它的內容通常是很難的（但收穫也同樣很多！）。然而，每次我們分析遇到的困難時，得到的結論都是應該將這種困難“歸咎於”實際討論的問題，而不是有關的文字本身（即它的表達方式）。它的寓意是，一個非平凡的算法本身就是非平凡的，而與論證其設計的正確性的思考相比，在一個程式語言里做出的算法描述是高度緊湊的：不要受到最後的程式正文長度的誤導！我的一個助理給出的建議——這也是我忠實地採納的，因為它可以很有價值——是讓學生分為一些小
組一起學習這本書。（在這裡，我必須對書中正文的“困難程度”加一點附帶的說明。我本人科學生涯中的許多年一直在致力於弄清楚程式設計師的任務，目標是設法使它成為智力上可以管理的工作。從事了多年的這種澄清性的工作之後，我感到好玩，也很吃驚地發現，反覆出現的回饋是“我把編程弄得更困難了”。但困難始終在那裡，只有將其變為明顯可見的，我們才有希望設計出具有高度信任水平的程式，而不僅僅是做出了一些“胡亂塗抹出的代碼”，即那種基於根本無法得到支持的假設，準備著被第一個反例推翻的程式正文。不用說，本書的任何一個程式都沒有在機器上測試過。）
我還要給讀者解釋為什麼我把這裡的小型語言弄得這么小，小到沒有包含過程和遞歸。由於任何一點語言擴充都會給這本書增加幾章內容，並因此使它也相應地變得更昂貴，所以對於大部分可能的擴充（例如多道編程），我都不需要更多的解釋。而過程總是在編程中居於核心的地位，遞歸對於計算科學而言也是最受學術界重視的標誌，因此，我必須給出一些解釋。
首先，這本專著不是為新手寫的，因此，我期望本書的讀者熟悉這些概念。其次，本書不是某個特殊程式語言的引論教材，缺乏這些結構和使用它們的例子，不會被解釋為我不能或者不希望使用它們，也不會被作為是建議那些有能力使用這些結構的人不要用它們。這裡的關鍵是我覺得在傳遞想給出的信息時我並不需要這些結構。我想討論的是應該仔細地分離各種關注，以及為什麼從各個方面看這種做法都是設計出高質量程式的最重要的基礎。以這裡的小型語言作為一種有節制的工具，對於給出各種非平凡而且非常令人滿意的設計而言，已經能給我們足夠的行動自由了。
前面的解釋雖然已經很充分，但還不是故事的全部。在任何情況下，我都覺得必須把重複結構本身作為語言中的一種結構，因為在我看來，這樣的闡釋是早就應該有的東西。當程式語言誕生時，其賦值語句的“動態”性質看起來與傳統數學的“靜態”性質很不吻合。由於沒有合適的理論，數學家就覺得很不喜歡它。而且，由於重複結構是需要變數賦值的最根本原因，數學家也很不喜歡重複結構。當人們開發出沒有賦值，也沒有重複結構的程式語言——例如，純LISP——時，許多人都大大地鬆了一口氣。這使他們又可以回到自己熟悉的場地里，看到了一點希望的微光：有可能將編程變成一種具有堅實的而且得到廣泛尊重的數學基礎的活動。
另一種角度就是為“重複結構”和“給變數賦值”提供一種可靠的而且可用的數學基礎，為此，我們又必須等待另一個十年。這方面研究的成果是，正如在這本專著里闡釋的，一個重複結構的語義可以基於謂詞之間的一個遞歸關係定義，而一個廣義遞歸的語義定義則需要基於謂詞轉換器之間的一個遞歸關係。這一點很清楚地說明，為什麼我認為廣義遞歸的複雜性比重複結構高一個數量級。因此，我很害怕看到將下面這樣重複結構的語義
定義為調用
其中的whiledo是如下定義的遞歸過程（用ALGOL 60的語法描述）
雖然這樣做不錯，但它卻傷到我了，因為我不喜歡用一把大錘去敲一個雞蛋，無論用大錘做這件事是多么的有效。對於在20世紀60年代涉足這一問題的那一代理論計算科學家來說，上面的定義常常不僅是“自然的那一個”，而且是“真正的那一個”。應該看到下面的事實：如果不訴諸重複的概念，我們甚至無法定義圖靈機能夠做什麼。這說明需要重新做一些權衡。
對於沒有參考文獻的問題，我不準備解釋，也不表示歉意。
