午後からIPAで形式手法のセミナーを受講。
形式手法入門−管理者向け半日コース
仕様を要求や設計などの上流工程で機械可読にすることで、建築における構造計算のように、仕様の品質をかっちりと計算できますよ、という話。（この構造計算の喩えは和歌山大学の鰺坂先生によるものだが、大変わかりやすかった。）
ソフトウェアの品質を検証する、という場合の「検証」は、多くの場合「verification」だが、形式手法は「validation」の意味での検証の手段ということのようだ。
管理者向けの話だったので、具体的な作業が見えていないのだが、理解するためには、結局はVDM++かなにかの仕様記述言語でコーディングしてみるべきなのだろう。
窓からスカイツリーが見えた。
