My last two entries were about Agile Software Design.
Would Agile Software Design be appropriate for designing safety-critical systems, such as firmware in medical devices, software for automated railroads, or spacecraft navigation? I do not think so.
This is where Formal Software Design Methods are used.
One expert in Formal Methods says that Formal Software Design Methods are “used by companies that produced safety-critical software where peoples lives are at stake.” (Eric Hehner)
Formal Software Design uses mathematics to prove program correctness. It is a rigorous method, requiring a background in math and software engineering.
Hehner says this about testing a computer program:
“When you are finished, you have to test your program to see if it's working. But how do you know if it's working? If it crashes, obviously it isn't working, but if it doesn't crash, how do you know if the answers it gives are correct? And you can test only some cases, not all of them, because there are too many to test. Maybe even infinitely many. There may be errors that would show up in the cases you didn't test. The only way is mathematical proof. Proof tells whether the program is correct for all inputs, even if there are infinitely many inputs.”
Eric Hehner