2011-12-12から1日間の記事一覧
概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するも…
目的 これに続く記事において、Krakatoa+Why3で証明を行うため。 想定環境 Ubuntu 11.10 (oneiric ocelot) なお、筆者の環境はamd64。 関連パッケージの準備 余計なのも書いてるかも。 $ sudo apt-get install build-essential devscripts dh-ocaml ocaml-no…