# HG changeset patch # User atton # Date 1485164483 -32400 # Node ID 36ce493604fbf037a18b53ec517f07e68ede677e # Parent 243d8dc4a2922558e1503881c8a9cc9a086ef042 Add akasha result diff -r 243d8dc4a292 -r 36ce493604fb paper/atton-master.tex --- a/paper/atton-master.tex Mon Jan 23 17:19:30 2017 +0900 +++ b/paper/atton-master.tex Mon Jan 23 18:41:23 2017 +0900 @@ -100,14 +100,7 @@ \input{introduction.tex} \input{cbc.tex} - -\chapter{ラムダ計算と型システム} -\label{chapter:type} -\section{型システムとは} -\section{型なしラムダ計算} -\section{単純型付きラムダ計算} -\section{部分型付け} -\section{部分型と Continuation based C} +\input{type.tex} \chapter{証明支援系言語 Agda による証明手法} \label{chapter:agda} diff -r 243d8dc4a292 -r 36ce493604fb paper/cbc.tex --- a/paper/cbc.tex Mon Jan 23 17:19:30 2017 +0900 +++ b/paper/cbc.tex Mon Jan 23 18:41:23 2017 +0900 @@ -260,6 +260,8 @@ % }}} +% {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証 + \section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} GearsOS の赤黒木の仕様の定義とその確認を CbC で行なっていく。 赤黒木には以下の性質が求められる。 @@ -303,7 +305,20 @@ \lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c} 同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。 +assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。 +\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 +検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。 +\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} -% TODO: meta の定義 -% TODO: akasha の結果 +これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 +検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 +実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。 +この \verb/meta/ が行なうのは検証用にメモリの管理である。 +状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。 +このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。 +また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。 + +\lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c} + +% }}} diff -r 243d8dc4a292 -r 36ce493604fb paper/src/akashaMeta.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/akashaMeta.c Mon Jan 23 18:41:23 2017 +0900 @@ -0,0 +1,31 @@ +__code meta(struct Context* context, enum Code next) { + struct Iterator* iter = &context->data[Iter]->iterator; + + switch (context->prev) { + case GoToPreviousDepth: + if (iter->iteratedPointDataNum == 0) break; + if (iter->iteratedPointHeap == NULL) break; + + unsigned int diff =(unsigned long)context->heap - (unsigned long)iter->iteratedPointHeap; + memset(iter->iteratedPointHeap, 0, diff); + context->dataNum = iter->iteratedPointDataNum; + context->heap = iter->iteratedPointHeap; + break; + default: + break; + } + switch (next) { + case PutAndGoToNextDepth: // with assert check + if (context->prev == GoToPreviousDepth) break; + if (iter->previousDepth == NULL) break; + iter->previousDepth->iteratedPointDataNum = context->dataNum; + iter->previousDepth->iteratedPointHeap = context->heap; + break; + default: + break; + } + + context->prev = next; + goto (context->code[next])(context); +} + diff -r 243d8dc4a292 -r 36ce493604fb paper/src/meta.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/meta.c Mon Jan 23 18:41:23 2017 +0900 @@ -0,0 +1,4 @@ +__code meta(struct Context* context, enum Code next) { + goto (context->code[next])(context); +} + diff -r 243d8dc4a292 -r 36ce493604fb paper/type.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/type.tex Mon Jan 23 18:41:23 2017 +0900 @@ -0,0 +1,14 @@ +\chapter{ラムダ計算と型システム} +\label{chapter:type} +\ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。 +しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。 +CbC は直接自身を証明する機構が存在しない。 +プログラムの性質を証明するには CbC の形式的な定義が必須となる。 +\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。 + + +\section{型システムとは} +\section{型なしラムダ計算} +\section{単純型付きラムダ計算} +\section{部分型付け} +\section{部分型と Continuation based C}