モデル検査
たまたまなのですが、たてつづけに「フルカバレッジのテストを行ったのと同等の証明をする手法がある」という話を聞く機会があり、一体どんなものなのだろう？と思っていたのですが、形式手法と呼ばれる方法のことらしいということがわかりました。
キーワードとしては、
- 形式手法
- モデル検査
- Model Checking
あたりで検索するといろいろ出てくるようです。
Model checking - Wikipedia, the free encyclopedia
話としては、
- アルゴリズムを仕様記述言語で記述する。
- そこからすべての状態遷移を力技で洗い出し、すべての状態が検証されているかをチェックする。
- 未検証の状態に落ちることはないということから、アルゴリズムに対しては数学的に妥当性検証済みといえる。
という話のようです。
