Coqによる 証明駆動開発 超入門証明駆動開発 とは 証明駆動開発 とは証明によってプログラムが期待通りの性質を有しているかを確かめながら開発する手法のこと。 ユニットテストの一部で使用可能な方法。 証明駆動開発 での流れは参考サイトに記載されているように以下の流れで行う。 1.対象プログラムが持つべき性質を洗い出す 2.Coqでプログラムを書く 3.書いたプログラムの性質を証明する 4.他の言語のコードに出力する 参考サイトに証明の仕方については記述されているため、このページでは 証明駆動開発 にのみ焦点を当てる。 参考になるサイト coqによる 証明駆動開発 とcoqideの使い方： http://d.hatena.ne.jp/zyxwv/20090922/1253643926coqtopの使い方： http://www.iij-ii.co.jp/lab/techdoc/coqt/coqtop-vimの使い方： htt
