6 posts
Cleanroom 驗證需要生成並消除證明義務（proof obligations）。以下說明 LLM 如何自動化註解與驗證條件（VC）的生成，讓你能專注於真正困難的證明工作。
Cleanroom 軟體工程要求你在編譯程式碼之前，先證明它是正確的。這聽起來很高尚，直到你花了三個小時為一個只排序十個整數的函式撰寫迴圈不變式（loop invariant）為止。 瓶頸不在證明本身，而在於那些繁瑣的樣板程式碼。生成驗證條件（verification…
Cleanroom software engineering 將 defect rate 降低 100 倍，但全面採用需要獨立的 test team 和 formal proof。這裡介紹一種 pragmatic subset，無需 overhead 即可捕獲大部分收益。
Cleanroom software engineering 每千行程式碼僅產生 0.1 個缺陷。業界平均水準是 10 到 50。問題是，完整的 Cleanroom 要求你將團隊拆分為 author 和 verifier，在每個 module 之前編寫 formal specification，並禁止…
IBM 的 Cleanroom engineering 達到了比業界平均水準好 100 倍的 defect rate，然後消失在歷史中。它的消失與是否有效毫無關係。
IBM 的 Cleanroom software engineering process 實現了每千行程式碼 0.1 個 defect。當時的業界平均水準在 10 到 50 之間。該 process 被文件化，在多個專案和語言之間 replicate，並經過獨立驗證。然後它消失了。 不是因為更好的 method…
Cleanroom software engineering 承諾透過 mathematical verification 而非 debugging 實現零缺陷增量。我們查看 IBM 的實際專案資料，看看這一說法是否成立。
1980 年代軟體業的平均水平是每千行程式碼 30 到 60 個缺陷。IBM 的 Cleanroom 團隊交付了一個 2 萬行的編譯器增量，在測試中發現了 53 個缺陷。也就是每 KLOC 2.6 個。一些 1 萬行的獨立增量在進入系統測試時，沒有發現任何缺陷。 最離奇的部分？程式設計師被禁止執行自己的程式碼。…
Box Structure 強制你將模組的行為、記憶的狀態和實作方式定義為三個獨立且可驗證的層。以下是 Cleanroom 如何利用它們消除除錯。
你先寫程式碼，再寫測試，然後發現程式碼是錯的。這是標準循環。也是為什麼除錯會消耗大多數專案時間線的一半。 Box Structure 把這個過程反轉。你在寫程式碼之前就定義行為，用數學方式驗證這個定義，然後一層一層翻譯成程式碼。結果是「構造即正確」的模組，而不是「測試碰巧通過所以正確」。…
IBM 的 Cleanroom 工程流程透過預防而非發現缺陷，達成了比業界平均好 100 倍的缺陷率。以下是它的運作方式、為何幾乎無人使用，以及你今天可以借鏡什麼。
IBM 交付了一套 NASA 衛星控制系統，每千行程式碼僅有 0.1 個缺陷。當時的業界平均水準在 10 到 50 之間。他們並非依靠招聘更聰明的工程師或延長工作時間來達成這項目標。他們靠的是禁止開發者執行自己的程式碼。 這就是 Cleanroom 軟體工程，由 IBM 的 Harlan Mills 於 1970…