探索 AI 優先開發、編碼護欄和可處置架構。
大型語言模型是發掘 test oracles 時還算稱職的腦力激盪夥伴，但它會幻覺化性質、遺漏領域限制。以下是如何安全使用它們，而不會上線錯誤的測試。
你需要測試一個無法事先知道正確輸出的函式。一個路徑最佳化器。一個情緒分類器。一個物理模擬。你讀過 metamorphic testing：找出輸入與輸出之間必須成立的關係，然後測試這些關係，而不是精確值。 問題在於想出這些關係。你盯著你的函式簽章，腦袋一片空白。 於是你去問 LLM。它在幾秒內丟回十個…
並非所有 metamorphic relations 都能抓到缺陷。弱的關係給你虛假的信心，強的關係才能找出真正的錯誤。以下是如何區分兩者，並建構一套真正有效的關係集合。
你為定價引擎寫了十二個 metamorphic relations。每個測試都通過。你對自己的涵蓋率感覺良好。 然後顧客回報大量折扣計算反了。你檢查你的關係套件。沒有任何一個測試失敗。你有加法一致性、單調性與idempotency的關係。沒有任何一個抓到折扣乘數的正負號錯誤。 這是 metamorphic…
Metamorphic testing 讓你在不知道預期輸出的情況下驗證程式碼正確性。以下是它的運作方式、限制，以及如何開始使用。
你上線了一個為支援工單標記分類的機器學習模型。你的測試套件全綠。每個測試都通過了。 那些測試沒有一個真正檢查標籤是否正確。你根本不知道正確的標籤是什麼。沒人知道。對於真實世界的輸入，「正確」的輸出實際上無法得知，所以你只好檢查函式不會崩潰，或者輸出形狀符合預期。這不是測試。這是在祈禱。 這就是 oracle…
如何運用 phantom types 與 `this` 參數，將非法的protocol轉換變成編譯期錯誤，而非執行期缺陷。
每個 API 用戶端內部都藏著一個state machine。先握手。再驗證。然後傳資料。最後關閉。打破這個順序，你就會得到執行期錯誤、困惑的伺服器，或者更糟——靜默的資料損毀。 大多數團隊用執行期檢查來編碼這些規則。。在某人忘記檢查之前都管用，或者一次 refactor…
OpenAPI 規格描述了請求與回應的 schema，但沒有規定合法的訊息順序。以下是能從中萃取什麼，以及哪些地方仍然需要手動補齊。
OpenAPI 規格會告訴你合法的請求長什麼樣子，以及合法的回應長什麼樣子。它不會告訴你，在呼叫 之前是否允許先呼叫 ，或者在你呼叫 之後再呼叫 會發生什麼事。這些資訊存在於protocol規格中，而 OpenAPI 並不是protocol規格。 這就是落差所在。你可以從 OpenAPI…
Session types 將通訊protocol編碼進型別系統，把執行期protocol錯誤變成編譯期失敗。以下是它們為何在研究論文裡待了三十年，才終於能進入正式產品程式碼。
Session types 發明於 1993 年。三十年後，大多數網路服務仍然用手寫的執行期檢查來驗證protocol狀態，如果它們會驗證的話。你的型別系統對於用戶端是否在 之前就傳送 ，或者是否因為有人忘了關閉連線而導致連線洩漏，完全無從置喙。 研究社群數十年前就有了對策。這從來不是理論問題。問題在於…
會話型別將通訊protocol編碼到你的型別系統中，在程式碼執行之前將訊息傳遞不匹配轉化為編譯器錯誤。
deadlock本應該是執行時期的問題。這就是讓它們如此煩人的原因。你的程式碼編譯乾淨，測試通過，然後它在生產環境中卡住，因為處理程序A在等待處理程序B，而處理程序B在等待處理程序A。…
如何使用Infer在CI管道中執行形式化靜態分析，包含可運作的組態設定和現實權衡。
抽象詮釋是那種會讓工程師關掉分頁的術語。它聽起來像是需要花一學期格論才能理解的東西。大多數開發者都以為它活在研究論文裡，而不是在提取要求中。…
大語言模型可以幫助分流靜態分析中的誤報，但它們無法像抽象詮釋那樣理解程式語義。以下是如何將兩者結合。
你的靜態分析器剛剛在一個週五下午發出了847條警告。從統計上看，其中大約5%到15%是真正的缺陷。其餘都是誤報：生成程式碼中的無效儲存、對工具來說可疑但對人類來說顯而易見的空值檢查、無關緊要的雜湊函式中的整數溢位。 手動逐一排查令人心力交瘁。於是你想：能不能直接問LLM哪些是真的？…
Facebook如何利用抽象詮釋和有意的不完整性，在數百萬行Android程式碼中大規模發現競態條件。
Facebook的Android應用程式有一個效能問題。UI執行緒被工作淹沒，但將程式碼移到背景執行緒意味著競態條件。投產當機。憤怒的使用者。…