A Role for Formal Methodists
Proving “correctness” of entire systems is not now feasible, nor is it likely to become feasible in the foreseeable future. Establishing that a large system satisfies a non-trivial specification requires a large proof. Without mechanical support, building or checking such a proof is not practical. Even with mechanical support, designing a large proof is at least as difficult as designing a large program. We are barely up to the task of building large and complex systems that almost work; we are certainly not up to building such systems twice — once in a programming language and once in a logic — without any flaws at all.
KeywordsModel Checker Formal Method Large System Mechanical Support Foreseeable Future
Unable to display preview. Download preview PDF.