ITpro連載 第13回 「表明」と「契約」による命令型プログラムの形式的検証
http://itpro.nikkeibp.co.jp/article/COLUMN/20070802/278931/?ST=develop
出ました。ホーア論理の話です。参考リンクにある京都賞受賞記念講演なども面白いかと思います。
記事にもある「形式的手法（数学的証明）によるプログラム検証」は、「バグがないことを保証する」みたいな言われ方をされますが（私もよくしてしまいますが）、「バグ」の意味が広範なために、「そんなことは不可能だ」という脊髄反射的な否定の原因になっている気もします。むしろ、「（有限の）テストケースによる抽出検査」と対比して、「（無限のテストケースも網羅できる）効率のよい全数検査」みたいな言い方をしたほうが通りやすい？
