Tech Tips

  1. Uncategorized
  2. 74 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.

Uncategorized recent post

  1. Run Amazon FreeRTOS on M5Stack Core2 for AWS …

  2. Udacity Self-Driving Car Engineer Nanodegree …

  3. Install sbt 1.0.0 and run sample template

  4. Visualization of Neural Network and its Train…

  5. [Machine Learning]Created docker image includ…

関連記事

PAGE TOP