本文為轉載 . 但在她之前有一點介紹。 喪屍是怎麼形成的？ 每個人都遇到過這樣一種情況，他們想把朋友或同事拉到他們的水平，但沒有成功。 與其說是你，不如說是他，“行不通”：天平的一邊是正常的薪水、任務等等，另一邊是思考的需要。 思考是不愉快和痛苦的。 他很快就放棄了，完全沒有動腦筋繼續寫代碼。 你想像需要付出多少努力才能克服習得性無助的障礙，但你就是不去做。 喪屍就是這樣形成的，看起來可以治愈，但似乎沒有人會去做。
當我看到那個 （是的，教科書上的同志） 而且不做報告，而是做問答環節，我有點警惕。 為了以防萬一，Leslie 是一位世界著名的科學家，分佈式計算基礎著作的作者，您也可以通過 LaTeX 中的字母 La 了解他 - “Lamport TeX”。 第二個令人擔憂的因素是他的要求：每個來的人都必須（絕對免費）提前聽他的一些報告，至少提出一個問題，然後才來。 我決定去看看 Lamport 在那裡廣播的內容 - 太棒了！ 正是那東西，治愈殭屍的神奇鏈接藥丸。 我警告你：從文本來看，超靈活方法論的愛好者和那些不喜歡測試所寫內容的人可能會特別疲倦。
實際上，在 habrokat 之後，研討會的翻譯就開始了。 享受閱讀！
無論你承擔什麼任務，你總是需要經曆三個步驟：
- 決定你想要達到的目標；
- 決定你將如何實現你的目標；
- 達到你的目標。
這也適用於編程。 在編寫代碼時，我們需要：
- 決定程序應該做什麼；
- 確定它應該如何執行任務；
- 編寫相應的代碼。
最後一步當然很重要，但今天不講。 相反，我們將討論前兩個。 每個程序員在開始工作之前都會執行它們。 除非您決定要編寫瀏覽器還是數據庫，否則您不會坐下來寫作。 必須存在對目標的特定想法。 你一定要考慮程序到底要做什麼，不要以某種方式編寫，希望代碼能以某種方式變成瀏覽器。
這個代碼預想究竟是如何發生的呢？ 我們應該為此付出多少努力？ 這完全取決於我們要解決的問題的複雜程度。 假設我們要編寫一個容錯的分佈式系統。 在這種情況下，我們應該在坐下來編寫代碼之前仔細考慮一下。 如果我們只需要將整數變量遞增 1 怎麼辦？ 乍一看，這裡的一切都是微不足道的，不需要思考，但後來我們記得可能會發生溢出。 因此，即使要了解一個問題是簡單還是複雜，您也首先需要思考。
如果你提前考慮問題的可能解決方案，就可以避免錯誤。 但這需要你的思路清晰。 為此，您需要寫下您的想法。 我真的很喜歡 Dick Guindon 的名言：“當你寫作時，大自然會告訴你你的想法是多麼草率。” 如果你不寫，你只認為你在思考。 你需要以規範的形式寫下你的想法。
規範執行許多功能，尤其是在大型項目中。 但我只會談論其中之一：它們幫助我們清晰地思考。 清晰地思考是非常重要的，也是相當困難的，所以在這裡我們需要任何幫助。 我們應該用什麼語言編寫規範？ 一般來說，這始終是程序員的第一個問題：我們將用什麼語言編寫。 沒有一個正確答案：我們要解決的問題太多樣化了。 對於某些人來說，TLA+ 是我開發的規範語言。 對於其他人，使用中文更方便。 一切都視情況而定。
更重要的是另一個問題：如何實現更清晰的思維？ 答：我們必須像科學家一樣思考。 這是一種在過去 500 年中證明了自己的思維方式。 在科學中，我們建立現實的數學模型。 天文學也許是嚴格意義上的第一門科學。 在天文學所用的數學模型中，天體表現為具有質量、位置和動量的點，儘管實際上它們是有山有海、有潮汐有潮汐的極其複雜的物體。 與其他任何模型一樣，此模型的創建是為了解決某些問題。 如果您需要尋找行星，這對於確定將望遠鏡指向何處非常有用。 但是如果你想預測這個星球上的天氣，這個模型就不行了。
數學使我們能夠確定模型的屬性。 科學表明這些屬性如何與現實相關。 讓我們談談我們的科學，計算機科學。 我們工作的現實是各種計算系統：處理器、遊戲機、計算機、執行程序等等。 我將討論在計算機上運行程序，但總的來說，所有這些結論都適用於任何計算系統。 在我們的科學中，我們使用許多不同的模型：圖靈機、部分有序的事件集等等。
什麼是程序？ 這是任何可以獨立考慮的代碼。 假設我們需要寫一個瀏覽器。 我們執行三個任務：我們設計程序的用戶視圖，然後我們編寫程序的高級圖，最後我們編寫代碼。 當我們編寫代碼時，我們意識到我們需要編寫一個文本格式化程序。 這裡我們又需要解決三個問題：確定這個工具返回什麼文本； 選擇格式化算法； 寫代碼。 此任務有其自己的子任務：正確地將連字符插入單詞中。 我們還分三個步驟解決了這個子任務——如您所見，它們在許多級別上重複。
讓我們更詳細地考慮第一步：程序解決了什麼問題。 在這裡，我們通常將程序建模為接受一些輸入並產生一些輸出的函數。 在數學中，函數通常被描述為一組有序的對。 例如，自然數的平方函數被描述為集合 {<0,0>, <1,1>, <2,4>, <3,9>, …}。 這種函數的域是每對第一個元素的集合，即自然數。 要定義一個函數，我們需要指定它的作用域和公式。
但是數學中的函數與編程語言中的函數不同。 數學要容易得多。 由於我沒有時間處理複雜的示例，讓我們考慮一個簡單的示例：C 中的函數或 Java 中返回兩個整數的最大公約數的靜態方法。 在這個方法的規範中，我們會寫：計算 GCD(M,N) 論據 M и N哪裡 GCD(M,N) - 一個函數，其域是整數對的集合，返回值是可被整除的最大整數 M и N. 這個模型與現實有什麼關係？ 該模型對整數進行操作，而在 C 或 Java 中我們有一個 32 位 int. 這個模型允許我們決定算法是否正確 GCD，但它不會防止溢出錯誤。 這將需要一個更複雜的模型，但沒有時間。
讓我們談談函數作為模型的局限性。 有些程序（如操作系統）不只是為某些參數返回某個值，它們可以連續運行。 此外，作為模型的功能不太適合第二步：規劃如何解決問題。 快速排序和冒泡排序計算的是同一個函數，但它們是完全不同的算法。 因此，為了描述程序的目標是如何實現的，我使用了一個不同的模型，我們稱之為標準行為模型。 其中的程序被表示為一組所有允許的行為，每個行為又是一個狀態序列，狀態就是對變量的賦值。
讓我們看看 Euclid 算法的第二步是什麼樣的。 我們需要計算 GCD(M, N). 我們初始化 M 作為 x和 N 作為 y，然後重複從較大變量中減去這些變量中較小的變量，直到它們相等。 例如，如果 M = 12和 N = 18，我們可以描述以下行為：
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
如果 M = 0 и N = 0？ 零可以被所有數字整除，所以在這種情況下沒有最大的除數。 在這種情況下，我們需要回到第一步問：我們真的需要為非正數計算 GCD 嗎？ 如果這不是必需的，那麼您只需要更改規範即可。
這裡我們應該稍微題外話一下生產力。 它通常以每天編寫的代碼行數來衡量。 但是如果你去掉了一定數量的行，你的工作就會更有用，因為你有更少的錯誤空間。 擺脫代碼的最簡單方法是第一步。 您完全有可能不需要您嘗試實現的所有花里胡哨的功能。 簡化程序和節省時間的最快方法就是不做不該做的事情。 第二步是第二個最省時的潛力。 如果你用寫的行來衡量生產力，那麼思考如何完成一項任務會讓你 生產力較低，因為你可以用更少的代碼解決同樣的問題。 我這裡不能給出準確的統計，因為我沒有辦法統計我在規範上花時間，也就是在第一步和第二步上沒有寫的行數。 而且這裡也不能設置實驗，因為在實驗中我們沒有權利完成第一步，任務是預先確定的。
非正式規範中的許多困難很容易被忽略。 編寫嚴格的功能規範沒有什麼難的，我不會討論這個。 相反，我們將討論為標準行為編寫強規範。 有一個定理說任何一組行為都可以使用安全屬性來描述 （安全） 和生存屬性 （活躍度）. 安全意味著不會發生任何不好的事情，程序不會給出錯誤的答案。 生存能力意味著遲早會有好事發生，即程序遲早會給出正確答案。 通常，安全性是一個更重要的指標，錯誤最常發生在這裡。 因此，為了節省時間，我不會談論生存能力，儘管它當然也很重要。
我們首先通過規定一組可能的初始狀態來實現安全性。 其次，每個狀態與所有可能的下一個狀態的關係。 讓我們像科學家一樣行動，用數學方式定義狀態。 初始狀態集由公式描述，例如，在 Euclid 算法的情況下： (x = M) ∧ (y = N). 對於某些值 M и N 只有一個初始狀態。 與下一狀態的關係用公式描述，其中下一狀態的變量寫有素數，當前狀態的變量不寫素數。 在歐幾里得算法的情況下，我們將處理兩個公式的析取，其中一個 x 是最大值，在第二個中 - y:
在第一種情況下，y 的新值等於 y 的先前值，我們通過從較大的變量中減去較小的變量得到 x 的新值。 在第二種情況下，我們做相反的事情。
讓我們回到歐幾里得算法。 讓我們再次假設 M = 12, N = 18. 這定義了一個單一的初始狀態， (x = 12) ∧ (y = 18). 然後我們將這些值代入上面的公式並得到：
這是唯一可能的解決方案： x' = 18 - 12 ∧ y' = 12我們得到了行為： [x = 12, y = 18]. 同樣，我們可以描述我們行為中的所有狀態： [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
在最後狀態 [x = 6, y = 6] 表達式的兩部分都是假的，所以它沒有下一個狀態。 所以，我們對第二步有一個完整的說明——正如你所看到的，這是很普通的數學，就像在工程師和科學家中一樣，而不是像在計算機科學中那樣奇怪。
這兩個公式可以組合成時序邏輯的一個公式。 她舉止優雅，好解釋，只是現在沒空理她。 我們可能只需要時序邏輯來實現活潑屬性，而不需要安全性。 我不喜歡這樣的時間邏輯，它不是很普通的數學，但在生動的情況下，它是一種必要的邪惡。
在歐幾里得算法中，對於每個值 x и y 具有獨特的價值 x' и y'，這使得與下一個狀態的關係為真。 換句話說，歐幾里得算法是確定性的。 要對非確定性算法建模，當前狀態需要有多個可能的未來狀態，並且每個非素數變量值都有多個素數變量值，以便與下一個狀態的關係為真。 這很容易做到，但我現在不舉例。
要製作工作工具，您需要形式數學。 如何使規范正式化？ 為此，我們需要一種正式的語言，例如， . Euclid 算法的規範在這種語言中看起來像這樣：
帶三角形的等號符號表示符號左側的值定義為等於符號右側的值。 本質上，規範是一個定義，在我們的例子中是兩個定義。 對於 TLA+ 中的規範，您需要添加聲明和一些語法，如上面的幻燈片所示。 在 ASCII 中，它看起來像這樣：
如您所見，沒有什麼複雜的。 可以測試 TLA+ 的規範，即繞過小模型中所有可能的行為。 在我們的例子中，這個模型將是某些值 M и N. 這是一種非常高效和簡單的完全自動的驗證方法。 也可以寫出形式化的真值證明，然後機械地檢查，但這需要很多時間，所以幾乎沒有人這樣做。
TLA+ 的主要缺點是它是數學，程序員和計算機科學家都害怕數學。 乍一看，這聽起來像個玩笑，但不幸的是，我是認真的。 我的同事剛剛告訴我他是如何嘗試向幾位開發人員解釋 TLA+ 的。 公式一出現在屏幕上，頓時就變成了呆呆的眼睛。 所以如果 TLA+ 嚇到你，你可以使用 ，它是一種玩具編程語言。 PlusCal 中的表達式可以是任何 TLA+ 表達式，即大體上可以是任何數學表達式。 此外，PlusCal 具有用於非確定性算法的語法。 因為 PlusCal 可以編寫任何 TLA+ 表達式，所以 PlusCal 比任何真正的編程語言都更具表現力。 接下來，PlusCal 被編譯成易於閱讀的 TLA+ 規範。 當然，這並不意味著複雜的 PlusCal 規範會變成 TLA+ 上的簡單規範——只是它們之間的對應關係很明顯，不會有額外的複雜性。 最後，該規範可以通過 TLA+ 工具進行驗證。 總而言之，PlusCal 可以幫助克服數學恐懼症，即使對於程序員和計算機科學家來說也很容易理解。 過去，我在上面發布算法有一段時間（大約 10 年）。
或許有人會反對說 TLA+ 和 PlusCal 是數學，而數學只對發明的例子有效。 實際上，您需要一種具有類型、過程、對像等的真實語言。 這是錯誤的。 以下是在亞馬遜工作的 Chris Newcomb 寫道： “我們已經在十個主要項目中使用了 TLA+，在每個項目中，使用它都對開發產生了重大影響，因為我們能夠在投入生產之前發現危險的錯誤，並且因為它給了我們所需的洞察力和信心在不影響程序真實性的情況下進行積極的性能優化”. 您經常會聽到，當使用形式化方法時，我們會得到低效的代碼——實際上，一切恰恰相反。 此外，有一種觀點認為，即使程序員確信形式化方法的用處，也無法說服管理者相信形式化方法的必要性。 紐科姆寫道： “現在管理人員都在大力推動編寫TLA+的規範，並專門為此分配時間”. 因此，當管理人員看到 TLA+ 正在發揮作用時，他們會很樂意接受它。 Chris Newcomb 大約六個月前（2014 年 14 月）寫了這篇文章，但據我所知，現在有 10 個項目使用了 TLA+，而不是 360 個。另一個例子與 XBox 360 的設計有關。一位實習生來到 Charles Thacker 和為內存系統編寫規範。 多虧了這個規範，才發現了一個原本不會被注意到的錯誤，因此每個 XBox XNUMX 在使用四個小時後都會崩潰。 IBM 工程師確認他們的測試不會發現此錯誤。
您可以在 Internet 上閱讀有關 TLA+ 的更多信息，但現在讓我們談談非正式規範。 我們很少需要編寫計算最小公約數之類的程序。 我們更經常編寫程序，例如我為 TLA+ 編寫的漂亮打印機工具。 經過最簡單的處理後，TLA+代碼大概是這樣的：
但在上面的示例中，用戶很可能希望連詞和等號對齊。 所以正確的格式看起來更像這樣：
讓我們來看另一個例子：
而這里相反，等號、加號、乘號在源碼中的排列是隨機的，所以最簡單的處理就足夠了。 一般來說，正確的格式沒有精確的數學定義，因為在這種情況下“正確”意味著“用戶想要什麼”，而這無法從數學上確定。
似乎如果我們沒有真值的定義，那麼規範就毫無用處。 但事實並非如此。 僅僅因為我們不知道一個程序應該做什麼並不意味著我們不需要考慮它是如何工作的——相反，我們必須付出更多的努力。 規範在這裡尤為重要。 結構化打印的最優方案是不可能確定的，但這並不代表我們完全不應該採用它，把代碼寫成意識流也不是什麼好事。 最後，我寫了一個包含六個規則的規範和定義 以評論的形式 在java文件中。 以下是其中一條規則的示例： a left-comment token is LeftComment aligned with its covering token. 這條規則是用數學英語寫的： LeftComment aligned, left-comment и covering token - 帶有定義的術語。 數學家就是這樣描述數學的：他們寫下術語的定義，並根據這些定義制定規則。 這樣一個規範的好處是，850 個規則比 850 行代碼更容易理解和調試。 我必須說編寫這些規則並不容易，調試它們需要花費大量時間。 特別是出於這個目的，我寫了一個代碼來報告使用了哪個規則。 由於我在幾個例子上測試了這六個規則，我不必調試 XNUMX 行代碼，而且發現錯誤也很容易。 Java 對此有很好的工具。 如果我剛剛編寫代碼，我會花費更長的時間，而且格式的質量也會更差。
為什麼不能使用正式的規範？ 一方面，正確的執行在這裡並不是太重要。 結構打印輸出肯定不會取悅任何人，所以我不必讓它在所有奇怪的情況下都能正常工作。 更重要的是我沒有足夠的工具。 TLA+ 模型檢查器在這裡沒有用，所以我必須手動編寫示例。
上述規格具有所有規格共有的特徵。 它比代碼更高級別。 它可以用任何語言實現。 任何工具或方法對編寫它都是無用的。 沒有編程課程可以幫助您編寫此規範。 並且沒有任何工具可以使此規范成為不必要的，當然，除非您正在編寫一種專門用於在 TLA+ 中編寫結構化打印程序的語言。 最後，本規範並未具體說明我們將如何編寫代碼，它僅說明了代碼的作用。 我們編寫規範是為了幫助我們在開始考慮代碼之前考慮清楚問題。
但是這個規範也有區別於其他規範的特點。 95% 的其他規范明顯更短更簡單：
此外，該規範是一組規則。 通常，這是規格不佳的標誌。 理解一組規則的後果是相當困難的，這就是為什麼我不得不花很多時間調試它們。 但是，在這種情況下，我找不到更好的方法。
關於連續運行的程序值得多說幾句。 通常，它們並行工作，例如操作系統或分佈式系統。 很少有人能在精神上或紙上理解它們，我不是其中之一，儘管我曾經能夠做到。 因此，我們需要能夠檢查我們工作的工具——例如 TLA+ 或 PlusCal。
如果我已經知道代碼究竟應該做什麼，為什麼還要編寫規範呢？ 事實上，我只是以為我知道。 此外，有了規範，局外人不再需要進入代碼來了解他到底做了什麼。 我有一個規則：不應該有一般規則。 這個規則有一個例外，當然，這是我遵循的唯一通用規則：代碼做什麼的規範應該告訴人們他們在使用代碼時需要知道的一切。
那麼關於思考，程序員究竟需要知道些什麼呢？ 對於初學者來說，和其他人一樣：如果你不寫，那麼在你看來，你只是在思考。 此外，您需要在編碼之前思考，這意味著您需要在編碼之前進行編寫。 規範是我們在開始編碼之前編寫的內容。 任何人都可以使用或修改的任何代碼都需要規範。 而這個“某人”可能就是代碼寫完一個月後的作者本人。 大型程序和系統、類、方法，有時甚至是單個方法的複雜部分都需要規範。 關於代碼究竟應該寫些什麼？ 您需要描述它的作用，即什麼對使用此代碼的任何人都有用。 有時可能還需要指定代碼如何實現其目的。 如果我們在算法課程中經歷過這種方法，那麼我們就稱它為算法。 如果它是更特別、更新穎的東西，那麼我們就稱它為高級設計。 這裡沒有形式上的區別：兩者都是程序的抽像模型。
您究竟應該如何編寫代碼規範？ 最主要的是：它應該比代碼本身高一級。 它應該描述狀態和行為。 它應該像任務要求的那樣嚴格。 如果您正在編寫有關如何執行任務的規範，您可以用偽代碼或使用 PlusCal 編寫它。 您需要學習如何在正式規範上編寫規範。 這將為您提供必要的技能，這些技能也將幫助您掌握非正式技能。 你如何學習編寫正式的規範？ 當我們學習編程時，我們編寫程序然後調試它們。 這裡也是一樣的：編寫規範，用模型檢查器檢查，並修復錯誤。 TLA+ 可能不是正式規範的最佳語言，另一種語言可能更適合您的特定需求。 TLA+的優勢在於它很好地教授了數學思維。
如何鏈接規範和代碼？ 借助鏈接數學概念及其實現的註釋。 如果您使用圖形，那麼在程序級別您將擁有節點數組和鏈接數組。 因此，你需要準確地寫出圖是如何被這些編程結構實現的。
需要注意的是，以上都不適用於實際寫代碼的過程。 當你寫代碼的時候，也就是你執行第三步的時候，你也需要思考，想通程序。 如果一個子任務被證明是複雜的或不明顯的，你需要為它寫一個規範。 但我不是在這裡談論代碼本身。 您可以使用任何編程語言、任何方法，這與它們無關。 此外，以上都沒有消除測試和調試代碼的需要。 即使抽像模型編寫正確，在其實現中也可能存在錯誤。
編寫規範是編碼過程中的一個附加步驟。 多虧了它，可以更輕鬆地發現許多錯誤——我們從亞馬遜程序員的經驗中了解到這一點。 有了規範，節目的質量就更高了。 那麼，為什麼我們經常沒有它們呢？ 因為寫作很難。 寫作很難，因為為此你需要思考，而思考也很困難。 假裝你的想法總是更容易。 這裡可以用跑步來類比——跑得越少，跑得越慢。 您需要鍛煉肌肉並練習寫作。 需要練習。
規格可能不正確。 您可能在某個地方犯了錯誤，或者需求可能已經改變，或者可能需要進行改進。 任何人使用的任何代碼都必須更改，因此遲早規範將不再與程序匹配。 理想情況下，在這種情況下，您需要編寫新的規範並完全重寫代碼。 我們非常清楚沒有人會那樣做。 實際上，我們修補代碼並可能更新規範。 如果這遲早會發生，那麼為什麼要編寫規範呢？ 首先，對於將要編輯你的代碼的人來說，規範中的每一個額外的單詞都是金子般的重量，這個人很可能就是你自己。 我經常因為在編輯代碼時沒有獲得足夠的規範而自責。 而且我編寫的規範比代碼還多。 因此，當您編輯代碼時，規範總是需要更新。 其次，隨著每次修訂，代碼變得更糟，變得越來越難以閱讀和維護。 這是熵的增加。 但是，如果您不從規範開始，那麼您編寫的每一行都將是一次編輯，並且代碼從一開始就會笨拙且難以閱讀。
如前所述 , 沒有計劃就沒有勝利，沒有計劃就沒有勝利. 他對戰鬥略知一二。 有一種觀點認為編寫規範是浪費時間。 有時確實如此，任務非常簡單，無需考慮。 但是你應該永遠記住，當你被告知不要寫規範時，你就是被告知不要思考。 你應該每次都考慮一下。 仔細思考任務並不能保證您不會犯錯誤。 眾所周知，沒有人發明魔術棒，編程是一項艱鉅的任務。 但如果你不把問題想透，你肯定會犯錯誤。
你可以在一個特殊的網站上閱讀更多關於 TLA+ 和 PlusCal 的信息，你可以從我的主頁去那裡 . 這就是我的全部，謝謝你的關注。
請注意，這是翻譯。 當您寫評論時，請記住作者不會閱讀它們。 如果你真的想和作者聊天，那麼他將參加將於 2019 年 11 月 12 日至 2019 日在聖彼得堡舉行的 Hydra XNUMX 大會。 可以購買門票 .
來源： www.habr.com