Production Level Knowledge & Tips

  1. 未分類
  2. 3 view

[Coq]Binarize with Proof Driven Development part1

Target

Try to develop function which binarize image with Proof Driven Development.

Coq

Target

Try to develop function which binarize image with Proof Driven Development.

Coq

Define binarization function with 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.
I think following things are needed for proofing.
  • Same element number with the list and the list after applying function.
  • The list which is applied the function has only 2 type value 0 or 255.
I’ll prove them from next.
Define binarization function with 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.
I think following things are needed for proofing.
  • Same element number with the list and the list after applying function.
  • The list which is applied the function has only 2 type value 0 or 255.
I’ll prove them from next.

未分類 recent post

  1. Install sbt 1.0.0 and run sample template

  2. Visualization of Neural Network and its Train…

  3. [Machine Learning]Created docker image includ…

  4. [Node.js]How to write batch script with Node.…

  5. [Hive]Get top n items for each category

関連記事

PAGE TOP