3 ms·
You need formal machine-checked verification (Coq, Isabelle). Unfortunately, this is not enough. You need a consistent and complete specification, too.
by qznc 14y ago
You need formal machine-checked verification (Coq, Isabelle).
Unfortunately, this is not enough. You need a consistent and complete specification, too.
- skew 14y agoThe first half is a bit easier - if you can show some implementation meets the specification it is at least consistent. The second isn't so clear, but sometimes you can get a bit more confidence by showing that other good properties are implied by the specification alone.