静的コード解析の会で停止性検証について発表してきた - ::Eldesh a b = LEFT a

静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました*1。
本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込んでみた」という感じでまとめてみました。(前日深夜から突貫だったので超眠かった…)

今回の発表で伝わったかは怪しいですが、停止性のために最低限の機能を導入し、既存の機能を活かした仕組みはとても素晴らしいと思います。
楽しい部分を端的に挙げると、

まぁこれだけ聞いても絶対分からないので、詳しく知りたい方はModular termination verificationを読みましょう。

前回に引き続きVeriFastの話ですが、今回の内容は前回と比べて取っつきにくい内容でした。
理論的にも難しい割には、そもそも停止性なんて検証して何がうれしいのかから分かりづらいと思い、検証のモチベーションから始めています。

VeriFastでは動的束縛を伴う(=関数ポインタを使った)関数の相互再帰関数といった、かなり複雑な関数の停止性を検証することが出来ます。が、発表としては面白い具体例をほとんど出せなかったのは悔やまれるところです。

他の人の発表では @tanaka_akr さんのCoq2Cの話を聞き逃したのが残念でした…。

このスライドでは序論といった範囲止まりですので、実際にC言語(あるいはJava)コードの停止性を検査するために覚えるべきことはもう少しあります。
次回はそのあたりまで理解して紹介できたらいいなぁという気持ちです。

あとは、今回の発表中から意図的に省いた単語として「整礎(関係|集合)」というモノがあるのですが、これは多重集合などと言うモノを持ち出した意味をはっきり述べるために必須の概念ですので、…勉強しておきます。はい。