Tech Tips

  1. プログラミング
  2. 211 view

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

やりたいこと

証明駆動開発で画像の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つかな。
次回以降でその証明をする。

プログラミングの最近記事

  1. PlatformIO IDE for VSCode を使用して VSCode で Ardu…

  2. ROS Docker イメージで発生した GPG error の解消方法

  3. Streamlit で訪れた国を色づけした世界地図を作成できるアプリケーションを作成してみ…

  4. M5Stack Core2 for AWS – ESP32 IoT開発キットで…

  5. D3.js v7 で点・線・テキスト・ツールチップ・ズームを設定する方法

関連記事

PAGE TOP