6 ms·
Would you say that this has limitations and it's not a silver bullet? Eg. What if your software added numbers, formal verification proved that your program was
by flashmob 9y ago
Would you say that this has limitations and it's not a silver bullet? Eg. What if your software added numbers, formal verification proved that your program was indeed correct because it added the numbers. However, it missed the requirement that you also had to do subtraction, which for some reason was omitted in the specification.
- mannykannot 9y agoYou would be no worse off in this situation. Writing a formal spec. arguably makes it harder to overlook such issues. Formal verification is good at catching things like off-by-one errors, where the problem is not in the spec.
- mathgenius 9y agoYes, I agree of course. Garbage-in-garbage-out has many manifestations.