テストでは2つの関数が等価であることは証明できない。では何ができるのか。
N-version programmingは実装が一致することを前提とする。テストがなぜ不十分なのか、SMT solverがいかにして等価性を実際に証明できるのか、そして「十分に良い」と「形式的に検証済み」の境界線をどこに引くべきかを見ていく。
n版システムを構築した。同じクリティカルな関数を3つの独立した実装で用意し、多数決で結果を選ぶvoterを置き、単一障害点を凌駕したという満足感に浸っている。 だが、あなたは関数が等価であることを証明していない。コンパイルが通ることを証明したにすぎない。 n-version…