changeset 13:fccf91d337c3

Writing section 3
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 01 Jul 2016 19:36:48 +0900
parents 96f146208607
children 784913eb2902
files paper/vmpcbc.tex
diffstat 1 files changed, 10 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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}