# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1467369408 -32400
# Node ID fccf91d337c3f8c99f448fff6f689d4571524bba
# Parent  96f14620860728913321f284f9c1404844aa559d
Writing section 3

diff -r 96f146208607 -r fccf91d337c3 paper/vmpcbc.tex
--- a/paper/vmpcbc.tex	Fri Jul 01 19:21:17 2016 +0900
+++ b/paper/vmpcbc.tex	Fri Jul 01 19:36:48 2016 +0900
@@ -114,6 +114,16 @@
 また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
 
 \section{メタ計算を用いたデータ構造の性質の検証}
+CbC で記述されさデータ構造と、それに対する処理の性質を実際に検証する。
+検証の対象として、当研究室で CbC を用いて開発している Gears OS における非破壊赤黒木を用いる。
+赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
+また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
+非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
+本論文ではどのような順番で木に要素を挿入してもバランスしていることを検証する。
+
+% メタ計算で実現するために必要なこと
+% cbmc じゃだめなこと
+
 \section{まとめと今後の課題}
 
 \begin{thebibliography}{9}