2011-12-12から1日間の記事一覧

Krakatoa and Jessieを用いた、Javaプログラムの正当性&安全性証明(アルゴリズムもあるよ!)

概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するも…

Why 2.30とWhy3のビルド&インストール (Ubuntu)

目的 これに続く記事において、Krakatoa+Why3で証明を行うため。 想定環境 Ubuntu 11.10 (oneiric ocelot) なお、筆者の環境はamd64。 関連パッケージの準備 余計なのも書いてるかも。 $ sudo apt-get install build-essential devscripts dh-ocaml ocaml-no…