正規(guī)方法：只是良好的工程實(shí)踐甥材？
是的。答案是肯定的性含。打臉了洲赵，Betteridge。
本周早些時(shí)候商蕴，我在 TLA+ 會(huì)議 2024 做了主題演講叠萍。我在演講中的信息是我長(zhǎng)期以來一直認(rèn)為的真理：正規(guī)方法是良好的軟件工程實(shí)踐的重要組成部分。如果你是一名軟件工程師绪商，尤其是從事大規(guī)模系統(tǒng)苛谷、分布式系統(tǒng)或關(guān)鍵低級(jí)系統(tǒng)工作的工程師，而沒有將正規(guī)方法作為你的方法的一部分部宿，你可能會(huì)浪費(fèi)時(shí)間和金錢。
因?yàn)閺母旧险f瓢湃，工程是優(yōu)化時(shí)間和金錢的練習(xí)理张。
“如果工程學(xué)不再被普遍認(rèn)為甚至被定義為建造的藝術(shù)，那就好了绵患。從某種重要意義上說雾叭，它更像是不建造的藝術(shù)；或者粗略但不無道理地定義落蝙，它是用一美元做好任何笨手笨腳的人可以用兩美元做的事情的藝術(shù)织狐。” — Arthur Wellington
乍一看筏勒，這可能顯得反直覺移迫。正規(guī)方法并不便宜，也不是特別容易管行，并且不適合每種軟件工程方法厨埋。合理地認(rèn)為，正式方法會(huì)增加成本捐顷，特別是非重復(fù)性工程成本荡陷。但我的經(jīng)驗(yàn)是，這并不是真的迅涮，有兩個(gè)原因废赞。首先是返工。軟件工程在工程領(lǐng)域中有點(diǎn)獨(dú)特叮姑，因?yàn)樵O(shè)計(jì)和建造往往同時(shí)發(fā)生唉地，而且很多建造可以在設(shè)計(jì)沒有深入之前就開始。這在電氣工程（設(shè)計(jì) PCB 或布線不能在設(shè)計(jì)完成之前進(jìn)行）、土木工程（在不知道要建什么之前開始土方工程是可能的渣蜗，但可靠的浪費(fèi)錢的方法）或機(jī)械工程中并不是真實(shí)的屠尊，等等。這是軟件的一個(gè)巨大優(yōu)勢(shì)——其可變性是其征服世界的原因之一——但也可以顯著增加設(shè)計(jì)迭代的成本耕拷，將設(shè)計(jì)迭代變成實(shí)施迭代讼昆。第二是變更成本。一旦 API 或系統(tǒng)有了客戶骚烧，改變它會(huì)變得更加昂貴和困難浸赫。這與 Hyrum 的定律根本相關(guān)：
有足夠多的 API 用戶后，無論你在合同中承諾什么：系統(tǒng)的所有可觀察行為都會(huì)被某人依賴赃绊。
隔離具有 API 的系統(tǒng)行為是個(gè)好主意既峡。事實(shí)上，我認(rèn)為這是所有軟件工程中最重要的想法之一碧查。Hyrum 的定律提醒我們這種方法的局限性：用戶最終會(huì)依賴于 API 的每一個(gè)可想象的實(shí)現(xiàn)細(xì)節(jié)运敢。這并不意味著改變是不可能的。在我的職業(yè)生涯中忠售，我參與了許多項(xiàng)目传惠，完全重新實(shí)現(xiàn)了 API 背后的系統(tǒng)。這僅僅意味著變更是昂貴的稻扬，并且諸如 API 之類的抽象并不能有效地改變這種現(xiàn)實(shí)卦方。
通過節(jié)省返工成本，并在早期解決接口變更泰佳，正規(guī)設(shè)計(jì)工作可以顯著提高軟件構(gòu)建過程的速度和效率盼砍。
什么樣的系統(tǒng)？
這似乎不適用于所有類型的軟件逝她。由快速發(fā)展的或難以正式化的用戶需求驅(qū)動(dòng)的軟件浇坐，從用戶界面和網(wǎng)站到定價(jià)邏輯實(shí)現(xiàn)，可能需要大量持續(xù)的返工黔宛，以至于前期設(shè)計(jì)的價(jià)值被稀釋（或其成本顯著增加）吗跋。這是敏捷背后的基本思想：通過并行運(yùn)行實(shí)現(xiàn)和需求收集，可以減少實(shí)際上市時(shí)間宁昭。更重要的是跌宛，在需求收集是一個(gè)持續(xù)過程時(shí)，它允許實(shí)現(xiàn)即使在需求不斷演變時(shí)也能完成积仗。在許多情況下疆拘，這種并行開發(fā)方法是最優(yōu)的，甚至是取得任何進(jìn)展所必需的寂曹。
另一方面哎迄，大規(guī)模回右、分布式和低級(jí)系統(tǒng)背后的許多軟件都有很好的需求理解∈浚或者至少翔烁，一個(gè)足夠大的已知靜態(tài)需求子集，使前期正式設(shè)計(jì)顯著減少了實(shí)現(xiàn)階段（以及之后旨涝，當(dāng)系統(tǒng)投入生產(chǎn)時(shí)）的返工和錯(cuò)誤密度蹬屹。
關(guān)于前期設(shè)計(jì)與敏捷之間的爭(zhēng)論大多來自于軟件光譜兩端的人們互相交談時(shí)互不理解。我們不應(yīng)該對(duì)需求收集模型非常不同的軟件有不同的最佳工程方法感到驚訝白华】看起來需求過程越接近物理定律，在工程過程中設(shè)計(jì)和正規(guī)設(shè)計(jì)就越有價(jià)值弧腥。需求越接近用戶意見厦取，它們就越不有價(jià)值。
這并不意味著明確寫下用戶需求沒有價(jià)值管搪，也不意味著探索正式指定它們的方法沒有價(jià)值虾攻。正式或非正式地寫下需求是極其有價(jià)值的。不寫下來可能會(huì)浪費(fèi)很多時(shí)間更鲁，并導(dǎo)致很多摩擦霎箍，因?yàn)槿藗冏罱K會(huì)朝不同方向拉動(dòng)。然而岁经，這確實(shí)意味著正式指定所有形式的人類需求通常很難（也許不經(jīng)濟(jì)）朋沮。例如蛇券，我不知道如何指定用戶界面美學(xué)要求缀壤、文檔可讀性甚至 API 命名一致性。
哪些工具纠亚？
正規(guī)方法和自動(dòng)推理是廣泛的領(lǐng)域塘慕，有大量工具。在我的職業(yè)生涯中蒂胞，在大型云系統(tǒng)領(lǐng)域中图呢，我發(fā)現(xiàn)以下工具有用（但我確信如果我知道它們，我會(huì)發(fā)現(xiàn)更多有用的工具）骗随。
- 像 P蛤织、TLA+ 和 Alloy 這樣的規(guī)格語言，以及它們相關(guān)的模型檢查器鸿染。
- 像 turmoil 這樣的確定性模擬工具指蚜，它們與模糊測(cè)試一起允許通過測(cè)試有原則地搜索狀態(tài)空間。
- 像 Dafny 這樣的驗(yàn)證感知編程語言和像 Kani 這樣的代碼驗(yàn)證器涨椒。我不是這些工具的深度專家摊鸡，用得少一些绽媒。
- 數(shù)值模擬技術(shù)。我傾向于自己構(gòu)建（如前所述）免猾，但市場(chǎng)上有許多框架和工具是辕。
- 白板上的準(zhǔn)正式方法。這些方法包括在白板上或設(shè)計(jì)文檔中繪制決策表猎提、真值表获三、顯式狀態(tài)機(jī)等。
我也喜歡《Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3》中的方法調(diào)查忧侧。這是一個(gè)很好的起點(diǎn)石窑。
但正如本文所述，我們不應(yīng)過于執(zhí)著于認(rèn)為驗(yàn)證實(shí)現(xiàn)是唯一有價(jià)值的最終目標(biāo)蚓炬。這確實(shí)是一個(gè)有價(jià)值的目標(biāo)松逊，但我發(fā)現(xiàn)使用像 TLA+ 和 P 這樣的工具在構(gòu)建之前更快、更具體地思考設(shè)計(jì)非常有價(jià)值肯夏。
更快的軟件经宏，更快
回到 2015 年，當(dāng)我們?yōu)?CACM 編寫《How Amazon Web Services Uses Formal Methods》時(shí)驯击，我非常關(guān)注正確性烁兰。關(guān)注驗(yàn)證設(shè)計(jì)的安全性和活性屬性，以及更快地獲得正確設(shè)計(jì)徊都。在與一個(gè)使用 TLA+ 內(nèi)部鎖管理系統(tǒng)團(tuán)隊(duì)交談時(shí)沪斟，我發(fā)現(xiàn)了一些我更喜歡的東西。
這令人耳目一新暇矫。不僅像 TLA+ 這樣的工具幫助我們更快地構(gòu)建系統(tǒng)主之，它們還幫助我們構(gòu)建更快的系統(tǒng)。它們?cè)试S我們快速探索可能的優(yōu)化李根，找到真正重要的約束槽奕，并檢查我們提出的優(yōu)化是否正確。在許多情況下房轿，它們消除了許多系統(tǒng)可能陷入正確性與性能之間艱難權(quán)衡的問題粤攒。
結(jié)論
在設(shè)計(jì)階段使用工具幫助我們思考系統(tǒng)設(shè)計(jì)可以顯著提高軟件開發(fā)速度、降低風(fēng)險(xiǎn)囱持，并允許我們從一開始就開發(fā)出更優(yōu)化的系統(tǒng)夯接。對(duì)于那些從事大規(guī)模和復(fù)雜系統(tǒng)工作的人來說，它們只是良好工程實(shí)踐的一部分纷妆。
