資源描述：
《引言(Introduction)》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在行業(yè)資料-天天文庫(kù)。
1、第零章序言(Preface)0.0引言(Introduction)程序設(shè)計(jì)理論有什么用?誰(shuí)需要它呢?沒有任何理論，成千上萬(wàn)的程序員還是每天都在編程,那么又何必費(fèi)心去學(xué)一門理論呢？該問(wèn)題的答案其實(shí)和任何其他理論一樣。譬如,為什么人人都要學(xué)習(xí)運(yùn)動(dòng)學(xué)理論?你可以在不懂理論的情況下行動(dòng)自如,也可以在不懂理論的情況下投球。但我們?nèi)匀徽J(rèn)為在中學(xué)講授運(yùn)動(dòng)學(xué)理論是相當(dāng)重要的。對(duì)這個(gè)的問(wèn)題的回答之一是,通過(guò)提供演算的方法，數(shù)學(xué)理論達(dá)到了一個(gè)高得多的精確程度。沒有關(guān)于運(yùn)動(dòng)學(xué)的理論,我們根本不可能發(fā)射火箭到木星。甚至
2、投球手們也發(fā)現(xiàn)理論專家可以幫助他們改進(jìn)投球技術(shù)。同樣,沒有理論的幫助,許多一般的程序設(shè)計(jì)也可以完成,但對(duì)更復(fù)雜的程序設(shè)計(jì),沒有好的理論就難以正確無(wú)誤的完成。軟件產(chǎn)業(yè)有數(shù)不清的因程序錯(cuò)誤造成的慘痛教訓(xùn)無(wú)一不證明了這點(diǎn)。況且,即使是通常的編程也會(huì)因適當(dāng)運(yùn)用理論而得到改進(jìn)。而回答之二是,理論可以提高理解能力。當(dāng)我們學(xué)會(huì)了運(yùn)動(dòng)學(xué)的理論時(shí),我們對(duì)運(yùn)動(dòng)的控制和預(yù)見能力從藝術(shù)走向了科學(xué)。同樣,當(dāng)我們學(xué)會(huì)以理解數(shù)學(xué)定理的方式來(lái)理解程序時(shí),程序設(shè)計(jì)也從藝術(shù)走向了科學(xué)。有了科學(xué)的觀點(diǎn),我們就改變了對(duì)世界的看法。更少
3、地依賴靈感或運(yùn)氣，更明白什么是可能的,什么是不可能的。對(duì)任何人而言，這都是通過(guò)寶貴的教育才能達(dá)到的。專業(yè)工程學(xué)在社會(huì)上維持很高的聲譽(yù),就是因?yàn)樗鼒?jiān)持這樣一點(diǎn):要成為一名專業(yè)工程師,一個(gè)人必須懂得和應(yīng)用相關(guān)的理論。一個(gè)土木工程師必須懂得和運(yùn)用幾何和材料力學(xué),一個(gè)電氣工程師必須懂得和運(yùn)用電磁理論,軟件工程師要想名副其實(shí),也必須懂得和運(yùn)用程序設(shè)計(jì)理論。本書的主題有時(shí)稱為“程序設(shè)計(jì)方法學(xué)”,有時(shí)又稱為“程序設(shè)計(jì)科學(xué)”,“程序設(shè)計(jì)邏輯”,“程序設(shè)計(jì)理論”,“程序開發(fā)形式化方法”,或“程序證明”,它涉及程序
4、設(shè)計(jì)中經(jīng)得起數(shù)學(xué)證明的那些方面。一個(gè)好的理論能幫助我們書寫精確的規(guī)范,并設(shè)計(jì)出其執(zhí)行可被證明滿足規(guī)范的程序。我們將考慮計(jì)算的狀態(tài)、計(jì)算的時(shí)間、計(jì)算的空間以及計(jì)算的交互。但有一些軟件設(shè)計(jì)和制作的重要方面本書沒有論及,例如人員管理,用戶界面,文檔化和測(cè)試等。第一個(gè)有用的程序設(shè)計(jì)理論通常稱為“Hoare邏輯”,仍可能是最廣為人知的。在Hoare邏輯中,一條規(guī)范是一對(duì)謂詞：前置條件和后置條件(這兩個(gè)術(shù)語(yǔ)及其后提及的所有術(shù)語(yǔ)都將在以后的相應(yīng)章節(jié)中給出定義)。另一個(gè)緊密相關(guān)的理論使用了Dijkstra的最弱
5、前置謂詞轉(zhuǎn)換器,它將程序和后置條件通過(guò)轉(zhuǎn)換得到前置條件，它后來(lái)發(fā)展成了Back的精化演算。Jones的維也納開發(fā)方法已被某些產(chǎn)業(yè)采用并獲益,其中,一條規(guī)范是一對(duì)謂詞(正如Hoare邏輯),但其中第二個(gè)謂詞是一個(gè)關(guān)系。另外，還有一些專門用于實(shí)時(shí)程序設(shè)計(jì)、概率程序設(shè)計(jì)、交互式程序設(shè)計(jì)的理論。本書中的理論比上面提到的都要簡(jiǎn)單。在該理論中,一條規(guī)范就是一個(gè)布爾表達(dá)式,精化就是通常的蘊(yùn)含式。該理論也比上述理論更為通用,同時(shí)適用于終止和非終止計(jì)算,順序和并行計(jì)算,以及獨(dú)立和交互式計(jì)算。我們可以同時(shí)有只對(duì)其初
6、值和終值感興趣的變量、對(duì)0其值始終感興趣的變量、只知道其可能值的變量和用于計(jì)算時(shí)間和空間的變量。它們都適合于同一理論中，其基礎(chǔ)在于將規(guī)范表示成布爾表達(dá)式，而布爾表達(dá)式的變量可以是任何感興趣的變量。有一種通過(guò)窮舉測(cè)試所有輸入來(lái)證明程序的方法，稱為模型檢測(cè)（modelchecking）。它優(yōu)于本書中理論的一點(diǎn)在于可以完全自動(dòng)化。通過(guò)明智的布爾表達(dá)式的表示（見練習(xí)6），60模型檢測(cè)當(dāng)前聲稱可以處理約10個(gè)狀態(tài)。這比宇宙中所估計(jì)的原子個(gè)數(shù)還多！這個(gè)數(shù)字60200令人印象深刻，可是后來(lái)我們意識(shí)到10約為2
7、，這意味這我們所談?wù)摰氖?00位二進(jìn)制數(shù)，也就是6個(gè)32位二進(jìn)制數(shù)變量的狀態(tài)空間。對(duì)任何一個(gè)超過(guò)六個(gè)變量的程序進(jìn)行模型檢測(cè)就需要抽象，每個(gè)抽象要求證明其保持所感興趣的性質(zhì)。這些抽象和證明不是自動(dòng)的。為了保證實(shí)用，模型檢測(cè)必須與其他的證明方法相結(jié)合，例如本書中的方法。本書還要一直強(qiáng)調(diào)的一點(diǎn)是，程序開發(fā)的每一步都是伴隨證明的，而不是在開發(fā)以后進(jìn)行證明。---------------------------------------------------------------------------
8、------------------------------------------------引言結(jié)束0.1當(dāng)前版本(CurrentEdition)在本書的當(dāng)前版本中，我們?cè)黾恿丝臻g約束和概率程序設(shè)計(jì)的新的資料，歸納了for循環(huán)規(guī)則，簡(jiǎn)化了對(duì)并發(fā)的處理，且對(duì)并行進(jìn)程之間的合作提供了選擇：通信（如第一版），和交互變量。本書加強(qiáng)了解釋和說(shuō)明，并增加了更多整理過(guò)的例子。在增加的同時(shí)，也有刪減。為了保證本書的精練，任何在課程中將略過(guò)的資料被刪除了。本書只有147頁(yè)，后面的只是練習(xí)和參考材料。授課教師可
