測試無法證明兩個函式等價。真正有用的是這個。
N-version programming 假設你的實作結果一致。我們來看看為什麼測試不夠、SMT solver 如何真正證明等價，以及該在「夠好就好」和「形式化驗證」之間劃下哪條界線。
你建了一個 n-version 系統。同一個關鍵函式的三份獨立實作、一個選出多數結果的 voter，以及一種自己已經搞定單點故障的溫暖感覺。 你並沒有證明這些函式是等價的。你只證明了它們編譯得過。 N-version programming 的概念是：如果其中一個實作有 bug，其他的大概不會有，所以 voter…