temporal-logic

無需學習時序邏輯即可對程式碼進行模型檢驗

像Kani這樣的有界模型檢驗器和像Alloy這樣的關係模型搜尋器，讓你能以普通的斷言和限制條件來驗證性質。你放棄了活性證明，換來的是以小時而非週為單位的學習曲線。

使用模型檢驗器不需要學習線性時序邏輯。Kani、CBMC和Alloy等工具讓你能以普通的斷言和關係限制條件來驗證性質。你放棄了證明活性性質的能力，換來的是以小時而非週為單位的學習曲線，而對於大多數軟體錯誤來說，這是一筆值得的交易。…