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

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

   Jul 13

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

by zuqqhi2 at 2013年7月13日
Pocket

やりたいこと

証明駆動開発で画像の2値化(白か黒の2種類の値のみにする)をする関数を作成してみる。

Coq

とりあえず2値化関数をCoqで定義する。

Require Import List.
Require Import Arith.

Fixpoint binarize (l : list nat)(th : nat) : list nat :=
  match l with
  | nil => nil
  | x::xs => if leb th x then 255 :: (binarize xs th) else 0 :: (binarize xs th)
  end.

証明が必要そうな内容は

  • 関数を適用する前と後で配列の要素数に変化がない
  • 関数適用後の配列には値が0か255の2種類しかない

の2つかな。
次回以降でその証明をする。

Related Posts

  • 2013年6月21日 [Coq]リストのモナドを定義してみる Coq リスト モナド リストモナドの定義 Haskellのモナドを定義してみることを考える。 まず、モナドに必要なのは以下の三つの性質である。 f(return(A),g) = g(A) f(A,return) = A f(f(A, g),h) = […]
  • 2015年3月25日 Coqによる 証明駆動開発 超入門 証明駆動開発 とは 証明駆動開発 とは証明によってプログラムが期待通りの性質を有しているかを確かめながら開発する手法のこと。 ユニットテストの一部で使用可能な方法。 証明駆動開発 […]
  • 2013年7月13日 [Haskell]画像処理 水平方向のエッジ やりたいこと 水平方向の微分で水平方向のエッジ画像を出力する。 プログラム プログラムはこんな感じ。 結果 入力画像 出力画像 Target Output horizontal edge image. Program […]
  • 2013年6月27日 [Javascript][Node.js][express]mongodbと連携させてみる mongodbを使って値の保存、読み出しを使ったプログラムを作成してみる。 まずは expressを使用してひな形を作成する。 次にmongodbとの接続に使用するモデルを作成する。 […]
  • [OpenCV][Ruby]Webページのデザイン崩れ確認の自動化2016年12月12日 [OpenCV][Ruby]Webページのデザイン崩れ確認の自動化 はじめに この記事は、OpenCV Advent Calendar […]
  • Windows上で Vagrant + Ansible を使ってテスト用Webサーバ構築2015年9月22日 Windows上で Vagrant + Ansible を使ってテスト用Webサーバ構築  Vagrantを使うことで仮想マシンを立ち上げることができる。Ansibleを使うことで立ち上げたマシンにソフトウェアをインストールさせたり、アプリをデプロイさせたりすることができる。本記事ではこれらのツールを使って、テスト用のWebサーバを立てる方法を紹介する。構 […]
Pocket

You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.