Mercurial > hg > Papers > 2017 > atton-master

comparison paper/cbc.tex @ 28:36ce493604fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add akasha result
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 23 Jan 2017 18:41:23 +0900
parents 243d8dc4a292
children 45d3ac176bf5
comparison
equal deleted inserted replaced
27:243d8dc4a292 28:36ce493604fb
258 258
259 \lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c} 259 \lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c}
260 260
261 % }}} 261 % }}}
262 262
263 % {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証
264
263 \section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} 265 \section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証}
264 GearsOS の赤黒木の仕様の定義とその確認を CbC で行なっていく。 266 GearsOS の赤黒木の仕様の定義とその確認を CbC で行なっていく。
265 赤黒木には以下の性質が求められる。 267 赤黒木には以下の性質が求められる。
266 268
267 \begin{itemize} 269 \begin{itemize}
301 葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。 303 葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。
302 304
303 \lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c} 305 \lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c}
304 306
305 同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。 307 同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。
306 308 assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。
307 309 \verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。
308 % TODO: meta の定義 310 検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。
309 % TODO: akasha の結果 311
312 \lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}
313
314 これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。
315 検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。
316 実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。
317 この \verb/meta/ が行なうのは検証用にメモリの管理である。
318 状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。
319 このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。
320 また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。
321
322 \lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c}
323
324 % }}}