プログラミング + アカデミック + 何か面白いこと

  1. Programming
  2. 26 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.

Programming recent post

  1. Install sbt 1.0.0 and run sample template

  2. [Machine Learning]Created docker image includ…

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

  4. [Play][Scala]Develop Request Driven Batch Usi…

  5. [OpenCV][Ruby]Auto check web page design corr…

関連記事

PAGE TOP