--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/tex/rbt_verif.tex	Tue Feb 09 18:44:53 2021 +0900
@@ -0,0 +1,11 @@
+\chapter{Red Black Tree の検証}
+
+Input Data Gear が Pre Condition を、 Output Data Gearが Post Condition を 満たしているか検証することで Hoare Logic に当てはめる。
+
+以下の要素を検証するための Meta Code Gear を実装する。
+
+
+そして、 Meta Code Gear から 生成される Meta Data Gear が Pre / Post Conditionを
+満たしているのか確認することで、関数一つ一つに対して Hoare Logic を用いた検証を行う
+
+