Krakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！) - 簡潔なQ概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。 この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するもの Why 2.30 および Why3 0.71 (両方必要) Why 2.30に同梱されているKrakatoa and Jessieを用いる。 Coq 上記ソフトウェアが動作するOS (ここではUbuntu 11.10) なお、Ubuntu上での準備方法は、直前の記事を参照。 流れ Javaコードに、KML(JMLをベースにした仕様記述言語)で仕様を付記する。 Krakatoaを使って、JavaコードをJessieコードに変換。(ちなみに、Cコード+ACSLをJ
