ズッキーニのプログラミング実験場

プログラミング + アカデミック + 何か面白いこと。 記載されているものは基本的に私が所属する団体とは関係がありません。

   Mar 25

Coqによる 証明駆動開発 超入門

証明駆動開発 とは 証明駆動開発 とは証明によってプログラムが期待通りの性質を有しているかを確かめながら開発する手法のこと。 ユニットテストの一部で使用可能な方法。 証明駆動開発 での流れは参考サイトに記載されているよう […]

続きを読む »

   Jul 13

[Coq]証明駆動開発で2値化 part1

やりたいこと 証明駆動開発で画像の2値化(白か黒の2種類の値のみにする)をする関数を作成してみる。 Coq とりあえず2値化関数をCoqで定義する。 証明が必要そうな内容は 関数を適用する前と後で配列の要素数に変化がない […]

続きを読む »

   Jun 21

[Coq]リストのモナドを定義してみる

Coq リスト モナド リストモナドの定義 Haskellのモナドを定義してみることを考える。 まず、モナドに必要なのは以下の三つの性質である。 f(return(A),g) = g(A) f(A,return) = A […]

続きを読む »