静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました*1。 本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込んでみた」という感じでまとめてみました。(前日深夜から突貫だったので超眠かった…) 今回の発表で伝わったかは怪しいですが、停止性のために最低限の機能を導入し、既存の機能を活かした仕組みはとても素晴らしいと思います。 楽しい部分を端的に挙げると、 多重集合のある種の順序関係からどんどん「関数を呼ぶ権利」が出てくる 関数の順序関係をコード上の大小関係で決めた まぁこれだけ聞いても絶対分からないので、詳しく知りたい方はModular termination verificationを読みましょう。 振り返り 前回に引き続きVeriFastの話ですが、今回の内容は前回と比べて取っつきにくい内容でした。