测试无法证明两个函数等价。以下方法才能真正做到。
N-version programming 假设你的实现结果一致。我们来看为什么测试远远不够，SMT solvers 如何真正证明等价性，以及如何在‘足够好’和形式化验证之间取舍。
你搭建了一个 n-version 系统。同一个关键函数的三个独立实现，一个选择多数结果的 voter，以及一种你已经规避了单点故障的满足感。 但你并没有证明这些函数是等价的。你只证明了它们能编译通过。 N-version programming 的核心思想是：如果某个实现存在 bug，其他实现大概率不会有，因此…