Are test cases required?
To be an “open proof”, no. You have to apply mathematical techniques in some way, but not test cases, to be an open proof. Now, to be high assurance, as a practical matter you need many test cases. Proofs are only as good as their assumptions, and test cases are very useful for partly checking many assumptions – including assumptions you didn’t realize you were making. Sometimes specifications have errors, and test cases can quickly spot many such errors. It turns out that traditional testing, plus the use of FM, make a really good team. Tests can only test very specific sets of inputs, and as noted above, they cannot even begin to test all possible inputs. So formal methods can check “all possible inputs” against specifications given certain assumptions, while test cases can be useful in checking the specifications and assumptions. But today, our problem isn’t really “how to test”. Most developers know (to at least some level) how to test programs, and there are many books and example
