本書將指導(dǎo)你如何使用TLA+語(yǔ)言編寫計(jì)算機(jī)系統(tǒng)規(guī)約。全書篇幅比較長(zhǎng)，但大多數(shù)人只需要閱讀第一部分的內(nèi)容就夠了，這部分包含了大多數(shù)工程師需要了解的與編寫規(guī)約有關(guān)的知識(shí)，至于學(xué)習(xí)它所需要的背景知識(shí)，只要求具備工程學(xué)或計(jì)算機(jī)科學(xué)的本科生所應(yīng)掌握的數(shù)學(xué)和計(jì)算機(jī)知識(shí)即可。第二部分將為需要進(jìn)階的讀者提供更深入的內(nèi)容。本書的其余部分是參考手冊(cè)——第三部分介紹TLA+工具，第四部分介紹TLA+語(yǔ)言本身。 TLA官網(wǎng)http://lamport.org有可供下載的配套資源，包括TLA+工具、練習(xí)、參考資料和勘誤清單。你也可以在搜索引擎上輸入uidlamporttlahomepage來找到上述頁(yè)面，但請(qǐng)不要把這個(gè)字符串放到互聯(lián)網(wǎng)上共享。 何為規(guī)約 寫作是發(fā)現(xiàn)你的想法有多么草率的根本方法。 ——Guindon 規(guī)約是“系統(tǒng)應(yīng)該做什么”的書面定義。定義一個(gè)系統(tǒng)有助于我們更好地理解它。在構(gòu)建系統(tǒng)之前最好先理解該系統(tǒng)，因此在實(shí)現(xiàn)之前先編寫系統(tǒng)規(guī)約是個(gè)好主意。 本書講述了系統(tǒng)的行為屬性，也可稱之為功能屬性或邏輯屬性。這些屬性定義系統(tǒng)應(yīng)該做什么。當(dāng)然系統(tǒng)還有其他我們這里不考慮的重要屬性，比如性能屬性。最差情況下的性能通常可以表示為行為屬性，在第9章我們講述了如何定義系統(tǒng)在一定時(shí)間內(nèi)的行為，不過，本書暫時(shí)不考慮如何定義平均性能。 我們編寫規(guī)約的基本工具是數(shù)學(xué)。數(shù)學(xué)是一門嚴(yán)謹(jǐn)?shù)恼Z(yǔ)言，比自然語(yǔ)言（例如英語(yǔ)或中文）更為精準(zhǔn)。在工程實(shí)踐中，不精準(zhǔn)就很容易出錯(cuò)，因此科學(xué)和工程學(xué)通常采用數(shù)學(xué)作為基本語(yǔ)言。 本書用到的數(shù)學(xué)語(yǔ)言會(huì)比你一直使用的數(shù)學(xué)語(yǔ)言更形式化一些。相對(duì)于形式化數(shù)學(xué)，大多數(shù)數(shù)學(xué)家和科學(xué)家在寫作中使用的數(shù)學(xué)表達(dá)方式并不十分精準(zhǔn)，應(yīng)用于小范圍還勉強(qiáng)可以，應(yīng)用于大范圍則不佳。在非形式化數(shù)學(xué)語(yǔ)言中，每個(gè)方程都是一個(gè)精確的斷言，但你必須閱讀方程前后的解釋性文字才能理解方程之間的關(guān)系以及定理的確切含義。邏輯學(xué)家已經(jīng)研究出了消除這些解釋性文字并使數(shù)學(xué)更形式化、更精準(zhǔn)完備的方法。 大多數(shù)數(shù)學(xué)家和科學(xué)家可能認(rèn)為形式化數(shù)學(xué)又長(zhǎng)又乏味，這是不對(duì)的，普通數(shù)學(xué)也可以用一種精準(zhǔn)完備的形式化語(yǔ)言來簡(jiǎn)潔表達(dá)。例如在第11章關(guān)于微分方程的Diffeential-Equations模塊中，只需要用20多行就可以定義任意微分方程的解。不過很少有規(guī)約需要用到如此深?yuàn)W的數(shù)學(xué)知識(shí)，大多數(shù)時(shí)候只需要簡(jiǎn)單應(yīng)用一些基礎(chǔ)數(shù)學(xué)概念即可。 為何是TLA+ 我們通過描述在執(zhí)行過程中可能會(huì)發(fā)生的行為來定義系統(tǒng)。1977年，AmirPnueli引入了時(shí)態(tài)邏輯（temporallogic）來描述系統(tǒng)行為。從理論上講，系統(tǒng)可以用單個(gè)時(shí)態(tài)邏輯公式表示，但在實(shí)際運(yùn)用上卻有些問題：它雖然能很理想地描述系統(tǒng)的某些屬性，但在描述其他屬性上卻不太方便。因此，我們通常將它與更傳統(tǒng)的系統(tǒng)表示方式結(jié)合在一起來定義系統(tǒng)。 也可稱為時(shí)序邏輯或時(shí)間邏輯，在本書中為了術(shù)語(yǔ)統(tǒng)一，均譯為時(shí)態(tài)邏輯�！�—譯者注 在20世紀(jì)80年代后期，我發(fā)明了TLA，即基于動(dòng)作（Action）的時(shí)態(tài)邏輯——這是Pnueli初始邏輯的簡(jiǎn)單變體。TLA使得用單個(gè)公式表示系統(tǒng)變得切實(shí)可行。TLA規(guī)約的大部分由普通的、非時(shí)態(tài)邏輯的數(shù)學(xué)公式組成，時(shí)態(tài)邏輯僅在其擅長(zhǎng)描述的屬性中引入并發(fā)揮作用。TLA還給出了一種很友好的系統(tǒng)推理模式，這種模式被稱為斷言式推理（assertionalreasoning），其在實(shí)踐中被證明是最有效的。不過，本書僅涉及規(guī)約本身，較少引入數(shù)學(xué)證明。 TLA+版本2對(duì)證明做了大量改進(jìn)，參見19.7節(jié)�！�—譯者注 時(shí)態(tài)邏輯使用了一套基本邏輯來表示普通數(shù)學(xué)，還有許多其他方法也可以使普通數(shù)學(xué)形式化。大多數(shù)計(jì)算機(jī)科學(xué)家都喜歡使用與他們熟悉的編程語(yǔ)言近似的語(yǔ)言，相反，我選擇了大多數(shù)數(shù)學(xué)家更喜歡的方法，邏輯學(xué)家將其稱為一階邏輯和集合論。 TLA為描述系統(tǒng)提供了數(shù)學(xué)基礎(chǔ)。要編寫規(guī)約，我們需要在此基礎(chǔ)上構(gòu)建完整的語(yǔ)言體系。我最初認(rèn)為該語(yǔ)言應(yīng)該是某種抽象的編程語(yǔ)言，其語(yǔ)義將基于TLA。一開始我不知道用哪種編程語(yǔ)言結(jié)構(gòu)最好，于是決定直接用TLA編寫規(guī)約，計(jì)劃在需要時(shí)再引入編程語(yǔ)言。令我驚訝的是，到后來我發(fā)現(xiàn)不需要了，我所需的就是一種編寫數(shù)學(xué)公式的健壯語(yǔ)言。 盡管數(shù)學(xué)家已經(jīng)發(fā)展了編寫公式的科學(xué)，但他們還沒有將其轉(zhuǎn)化為工程學(xué)科，他們?yōu)樾∫?guī)模的數(shù)學(xué)模型開發(fā)了符號(hào)語(yǔ)言，但對(duì)于大型應(yīng)用還沒有好的方法，因?yàn)檎鎸?shí)系統(tǒng)的規(guī)約可能長(zhǎng)達(dá)數(shù)十頁(yè)甚至數(shù)百頁(yè)。數(shù)學(xué)家知道如何編寫20行的公式，但對(duì)長(zhǎng)達(dá)20頁(yè)的公式卻束手無策。因此，我不得不在語(yǔ)言中引入書寫長(zhǎng)公式的符號(hào)方法，這些方法的形成得益于我從編程語(yǔ)言中學(xué)到的將大型規(guī)約模塊化的思路。 我將這種語(yǔ)言稱為TLA+。在編寫不同離散系統(tǒng)的規(guī)約時(shí)，我不斷對(duì)TLA+進(jìn)行提煉和改進(jìn)，直到后來TLA+趨于穩(wěn)定。我發(fā)現(xiàn)TLA+可以很好地定義從應(yīng)用程序接口（API）到分布式系統(tǒng)的各種系統(tǒng)。它可以用來為幾乎任何類型的離散系統(tǒng)編寫精準(zhǔn)的形式化定義，尤其適合描述異步系統(tǒng)，即組件運(yùn)行不嚴(yán)格遵循鎖步操作（lock-step）的系統(tǒng)。 關(guān)于本書 本書的第一部分包括第1～7章，是本書的核心，需要從頭到尾閱讀。它描述了如何定義稱為安全屬性的一類屬