\documentclass[submit,PRO]{ipsj}
\usepackage{PROpresentation}
\PROheadtitle{2016-2-(5): 情報処理学会プログラミング研究会 発表資料 2016年8月10日}

\usepackage[dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{listings}
\usepackage[font=bf,skip=\baselineskip]{caption}
\captionsetup[lstlisting]{font={small,tt}}
\lstset{
  language={C},
  basicstyle={\scriptsize},
  commentstyle={\scriptsize\itshape},
  keywordstyle={\scriptsize\bfseries},
  stringstyle={\scriptsize},
  frame={trlb},
  breaklines=true,
  columns=[l]{fullflexible},
  xrightmargin=0zw,
  xleftmargin=3zw,
  lineskip=-0.5ex,
  captionpos=b,
  moredelim=**[s][\color{red}]{\"compressed}{\"},
}
\renewcommand{\lstlistingname}{図}

\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}

\setcounter{巻数}{57}
\setcounter{号数}{1}
\setcounter{page}{1}

\受付{2015}{3}{4}
%\再受付{2015}{7}{16}   %省略可能
%\再再受付{2015}{7}{20} %省略可能
\採録{2015}{8}{1}


\begin{document}
\renewcommand{\thelstlisting}{\thesection-\arabic{lstlisting}}

\title{Continuation based C を用いたプログラムの検証手法}
\etitle{Verification method of programs using Continuation based C}

\affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\
Infomation Engineering Course Graduate School of Engineering and Science University of the Ryukyus}
\affiliate{RUniv}{琉球大学\\
University of the Ryukyus}


\author{比嘉 健太}{Yasutaka HIGA}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
ソフトウェアが期待される仕様を満たしているか調べることは重要である。
特に実際に動作しているソフトウェア自体を検証できると良い。
従来はassertなどを用いて検証しているが、モデル検査のような網羅的な検査を行うことはできない。
そこでソフトウェアの実行自体を網羅的に行うように変更する。
これは計算自体を変更するのでメタ計算となる。
本論文ではプログラムを Continuation based C (CbC) で記述する。
CbC では Code Segment という単位で処理を記述する。
CbC を用いることによりメタ計算は CbC の Code Segment 間に Meta Code Segment を挟むという単純な方法で実現できる。
そして、通常計算との切り替えも簡単に行うことができる。
ここでは、赤黒木を実際の例題として検証した。
比較対象としてANSI-Cの記号実行を行うCBMCでも検証する。
CBMCよりも広い範囲の検査が行えることを確認した。
\end{abstract}

\begin{jkeyword}
プログラミング言語, 検証, 赤黒木
\end{jkeyword}

\begin{eabstract}
Checking desirable specifications of software is important.
If it checks actual implementations, much better.
Currently, assertions in the implementations is used, but it does not verify all possible executions like a model checker.
We propose a modification of program executions to do the verification.
This kind of modification is called a meta computation.
In this paper, we describe programs in Continuation based C(CbC).
CbC programs is composed of Code Segments.
Using CbC, meta computations is easily implemented as an insertion of meta code segment between normal level code segments.
Red-black Tree is verified by with our method.
We also check it with CBMC which execute ANSI-C programs symbolically.
Our method covers wider range of execution of the program.
\end{eabstract}

\begin{ekeyword}
Programming Language, Verification, Red-Black Tree
\end{ekeyword}

\maketitle

\section{ソフトウェアの検証}
ソフトウェアの規模が大きくなるにつれ、バグは発生しやすくなる。
バグとはソフトウェアが期待される動作とは異なる動作を行なうことである。
ソフトウェアの期待される動作は仕様と呼ばれ、自然言語や論理で記述される。
検証とは、ソフトウェアが定められた環境下において仕様を満たすことを保証するものである。
ソフトウェアの検証手法には、定理証明とモデル検査がある。
定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その式が常に真であることを証明する。
定理証明を行なう言語には依存型で証明を行なう Agda\cite{cite:agda} や Coq\cite{cite:coq} などが存在する。
モデル検査はソフトウェアの全ての状態において仕様が満たされるかを確認するものである。
モデル検査器には、 Promela と呼ばれる言語でモデルを記述する Spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、ANSI-Cを記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
証明やモデル検査器で検証を行なう際、実際に動作するコードでなく検証用にコードを書き直す必要があるなど、実際の実装との乖離が存在する。
よって、書き直した記述では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
本研究は実際に動作するプログラムの信頼性を保証することを目的とする。

\section{Code SegmentとData Segment}
動作するコードを検証しやすい単位で記述するために本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。
Code Segmentとは処理の単位であり、ループを含まないような単純な処理のみを行なう。
プログラムはCode Segmentどうしを組み合わせることで構築される(図\ref{fig:csds})。
Code Segment間における値の受け渡しには、Data Segmentというデータの単位で行なう。
なお、接続されたCode Segmentには依存関係が発生するが、依存関係が無いCode Segmentは並列に実行することが可能である。

\begin{figure}
    \begin{center}
        \includegraphics[scale=0.5]{fig/code_segment_data_segment.pdf}
        \caption{Code Segmentどうしの組み合わせ}
        \label{fig:csds}
    \end{center}
\end{figure}

ここで、Code Segmentどうしの接続処理について考える。
処理を表すCode Segmentどうしの接続も処理である。
このような、計算を実現するための計算をメタ計算と呼ぶ。
メタ計算は Code Segment で記述することが可能であり、メタ計算を記述したCode SegmentをMeta Code Segmentと呼ぶ。
Meta Code SegmentはCode Segment間に存在する上位の処理と考えることもできる(図\ref{fig:metaCSDS})。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.45]{fig/meta_code_segment_and_meta_data_segment.pdf}
        \caption{Meta Code Segment と Meta Data Segment}
        \label{fig:metaCSDS}
    \end{center}
\end{figure}

また、メタ計算に必要なデータはMeta Data Segmentに格納し、通常の処理に必要なData Segmentも内包する。
プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。

\section{Continuation based C}
Code SegmentとData Segmentを用いたプログラミングスタイルで記述する言語として Continuation based C\cite{cite:cbc-clang} を作成した。
Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えたものである。
Code Segmentどうしの接続は goto による軽量継続で表される(図\ref{src:simpleCs})。
軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。
なお、C言語の資産を利用するために関数呼び出しを行なうことも可能である。
また、Code Segment のみが導入されたCbCで検証を行った例として Dining Philosophers Problem のデッドロック検知\cite{cite:dpp}がある。

% {{{ Code Segment の接続(10加算して2倍する)
\begin{figure}[ht]
\begin{lstlisting}
__code addTen(int a) {
    int b = a+10;
    goto twice(b);
}

__code twice(int x) {
    int y = 2*x;
    goto showValue(y);
}
\end{lstlisting}

\caption{Code Segment の接続(10加算して2倍する)}
\label{src:simpleCs}
\end{figure}
% }}}

CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
図\ref{src:simpleCs}の例では、\verb/addTen/ と \verb/twice/という2つのCode Segmentを定義している。
\verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
\verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。

また、CbCにおけるData SegmentはC言語における構造体と共用体を用いたデータ構造である。
各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(図\ref{src:simpleDs})。

% {{{ Data Segment の例
\begin{figure}[ht]
\begin{lstlisting}
union Data {
    struct Count {
        int x;
    } count;
    struct Port {
        int port;
    } port;
};
\end{lstlisting}
\caption{Data Segmentの例}
\label{src:simpleDs}
\end{figure}
% }}}

図\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。

Code Segment 内部ではポインタ演算は行なわず、メタ計算でポインタへの演算を行なう。
これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。
Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(図\ref{src:stub} における \verb/twice_stub/)。
CbC における Meta Code Segment は Code Segment と Code Segment 間に存在する Code Segment である。

% {{{ Data Segment を指定する Meta Code Segment
\begin{figure}[ht]
\begin{lstlisting}
// Code Segment
__code addTen(union Data* ds, int a) {
    int b = a+10;
    goto twice_stub(ds);
}

// Meta Code Segment
__code twice_stub(union Data* ds) {
    goto twice(ds->count.x);
}

// Code Segment
__code twice(int x) {
    int y = 2*x;
    goto showValue(y);
}
\end{lstlisting}
\caption{Data Segment を指定する Meta Code Segment}
\label{src:stub}
\end{figure}

% }}}

CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(図\ref{src:meta} の Context)。
また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(図\ref{src:meta} の \verb/meta/)。
\verb/meta/ を切り替えることで Code Segment を変更することなくメタ計算のみを変更することができる。

% {{{ メタ計算を用いてCode Segment を接続する例

\begin{figure}[ht]
\begin{lstlisting}
// Meta Data Segment
struct Context {
    union Data *data;  // Data Segment
    unsigned int gotoCount; // メタ計算に必要なデータ
    unsigned int stepOfAddTen;
};

// Meta Code Segment
__code meta(struct Context* context,
            enum Code next) {
    countext.gotoCount++;

    /* 接続時に行なうメタ計算を記述 */
    switch (next) {
        case AddTen:
            // 特定のCode Segmentへのメタ計算
            context.stepOfAddTen++;
            goto addTen_stub(context);
        case Twice:
            goto twice_stub(context);
    }
}

// Code Segment
__code addTen(struct Context* context, int a) {
    x = x+10;
    goto meta(context, Twice);
}

// Code Segment
__code twice(struct Context* context, int x) {
    x = x*2;
    goto meta(context, ShowValue);
}
\end{lstlisting}
\caption{メタ計算を用いてCode Segment を接続する例}
\label{src:meta}
\end{figure}

% }}}

メタ計算の例として、メモリ管理の他にも例外処理や並列実行、ネットワークアクセスなどがある。
通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。


\section{CbC で記述した非破壊赤黒木}
CbC で記述されたデータ構造に赤黒木がある。
赤黒木とは木構造のデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
赤黒木は通常の二分探索木としての条件の他に以下の条件を持つ。

\begin{itemize}
    \item 各ノードは赤または黒の色を持つ。
    \item ルートの色は黒である。
    \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)。
    \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
\end{itemize}

これらの条件により、木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる。

赤黒木の実装として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os} における非破壊赤黒木\cite{cite:rbtree}がある。
非破壊赤黒木とは木への挿入や削除を行なった際、一度構築した木構造を破壊せず新しく木構造を生成する赤黒木である。
非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することである(図\ref{fig:tree})。

\begin{figure}[ht]
    \begin{center}
        \includegraphics[scale=0.4]{fig/nondestructive_tree_modification.pdf}
        \caption{非破壊赤黒木の編集}
        \label{fig:tree}
    \end{center}
\end{figure}

関数呼び出しが可能な言語では再起呼び出しで木を辿ることか可能だが、CbC は \verb/goto/による軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
辿った経路を記憶するため Meta Data Segment にスタックを持たせる(図\ref{src:stack}における Context 内部の \verb/node_stack/)。
赤黒木で利用する Data Segment を図\ref{src:stack}に表す。
Data Segment は各ノードの情報を持つ \verb/Node/ と赤黒木を格納する \verb/Tree/と、挿入などの操作中の一時的な木を持つ\verb/Traverse/の共用体で表される。

% {{{ 赤黒木の Data Segment

\begin{figure}[ht]
\begin{lstlisting}
// Data Segment for Red-Black Tree
union Data {
    struct Tree {
        struct Node* root;
    } tree;
    struct Traverse {
        struct Node* current;
        int result;
    } traverse;
    struct Node {
        int key;
        union Data* value;
        struct Node* left;
        struct Node* right;
        enum Color {
            Red,
            Black,
        } color;
    } node;
};

// Meta Data Segment
struct Context {
    stack_ptr node_stack;
    union Data **data;
};
\end{lstlisting}
\caption{赤黒木の Data Segment}
\label{src:stack}
\end{figure}

% }}}

CbCによる赤黒木実装の例として、赤が続かないという制約をチェックする Code Segment を図\ref{src:rbtree}に示す。
まず、赤が連続するか判定するために親の情報が必須なため、経路を記憶しているスタックから親の情報を取得する。
親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。
親の色が赤である場合は次の条件判定へと \verb/goto/ するが、経路情報を再現するためにスタックへと親を再度挿入しつつ \verb/goto/ する。

% {{{ 赤黒木で赤のノードが続かないという制約の判定

\begin{figure}[ht]
\begin{lstlisting}
// Meta Code Segment
__code insertCase2(struct Context* context, struct Node* current) {
    struct Node* parent;
    stack_pop(context->node_stack, &parent);
    if (parent->color == Black) {
        stack_pop(context->code_stack, &context->next);
        goto meta(context, context->next);
    }
    stack_push(context->node_stack, &parent);
    goto meta(context, InsertCase3);
}

// Meta Meta Code Segment
__code insert2_stub(struct Context* context) {
    goto insertCase2(context, context->data[Traverse]->traverse.current);
}
\end{lstlisting}
\caption{赤黒木で赤のノードが続かないという制約の判定}
\label{src:rbtree}
\end{figure}

% }}}

ここで、赤黒木に対する処理を Code Segment とした場合、赤黒木のメモリ管理などは Meta Code Segment である。
赤黒木を利用する Code Segment からは赤黒木の処理は意識する必要がないため、赤黒木の処理はMeta Code Segment のように見え、赤黒木のメモリ管理は Meta Meta Code Segment と考えられる。
このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能である。

\section{メタ計算を用いた赤黒木の検証}
CbC で記述された赤黒木と、それに対する処理の性質を実際に検証していく。
赤黒木に求められる性質には以下のようなものがある

\begin{itemize}
    \item 挿入したデータを参照できること
    \item 削除したデータは参照できないこと
    \item 値を更新した後は更新された値が参照されること
    \item 操作を行なった後の木はバランスしていること
\end{itemize}

本論文では操作を挿入に限定し、任意の順で木に要素を挿入しても木がバランスすることを検証する。
検証には当研究室で開発している検証用メタ計算ライブラリ akasha を用いる。
akasha では仕様を Meta Code Segment に記述するため、CbCで常に真となる式として定義する
赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(図\ref{src:specification})。

% {{{ 木の高さの仕様記述

\begin{figure}[ht]
\begin{lstlisting}
if (akashaInfo.maxHeight >
    2*akashaInfo.minHeight) {
   goto meta(context, ShowTrace);
}
\end{lstlisting}
\caption{木の高さの仕様記述}
\label{src:specification}
\end{figure}

% }}}

図\ref{src:specification}で定義した仕様が常に成り立つか、全ての挿入順の組み合わせを列挙しながら確認していく。
無限回の挿入順番を数え上げることは状態の抽象化無しには不可能なので、限られた要素数の挿入を検証する。
検証の対象である赤黒木を内包する Meta Data Segment を定義し、挿入順の列挙に必要なデータを追加で定義する(図\ref{src:akashaDs})。
検証に必要なデータには挿入順の数え上げに使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/がある。

% {{{ akasha の Data Segment
\begin{figure}[ht]
\begin{lstlisting}
// Data Segment
union Data {
    struct Tree { /* ... */ } tree;
    struct Node { /* ... */ } node;

    /* for verification */
    struct IterElem {
        unsigned int val;
        struct IterElem* next;
    } iterElem;
    struct Iterator {
        struct Tree* tree;
        struct Iterator* previousDepth;
        struct IterElem* head;
        struct IterElem* last;
        unsigned int  iteratedValue;
        unsigned long iteratedPointDataNum;
        void*         iteratedPointHeap;
    } iterator;
    struct AkashaInfo {
        unsigned int minHeight;
        unsigned int maxHeight;
        struct AkashaNode* akashaNode;
    } akashaInfo;
    struct AkashaNode {
        unsigned int       height;
        struct Node*       node;
        struct AkashaNode* nextAkashaNode;
    } akashaNode;
};
\end{lstlisting}
\caption{akasha の Data Segment}
\label{src:akashaDs}
\end{figure}

% }}}

挿入順の数え上げには深さ優先探索を用いるが、CbCスタックフレームが無いために再帰では記述できず、データ構造に今の状態を保持させながら探索する。
検証する要素を全て持つ環状リストを作成し、木に一度挿入する度に挿入した要素を排除した環状リストを複製していく。
環状リストに全ての要素が無くなった時、1つの組み合わせを列挙したことになる。
1つの挿入順を列挙後、前の深さの環状リストを再現し、環状リストの先頭を進めることで組み合わせの列挙を続ける。

挿入順を列挙しつつ、木に要素を挿入する度に図\ref{src:specification}の仕様が成り立つか Code Segment を実行して確認する。
仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(図\ref{src:getMinHeight})。

% {{{ 木の最も低い高さを取得する Code Segment

\begin{figure}[ht]
\begin{lstlisting}
__code getMinHeight(struct Context* context,
                    struct AkashaNode* left,
                    struct AkashaNode* right,
                    struct AkashaInfo* ai) {
    const struct AkashaNode* an = ai->akashaNode;

    if (an == NULL) {
        ai->akashaNode->height = 1;
        ai->akashaNode->node   = context->data[Tree]->tree.root;

        goto getMaxHeight_stub(context);
    }

    const struct Node* n = ai->akashaNode->node;
    if (n->left == NULL && n->right == NULL) {
        if (ai->minHeight > an->height) {
            ai->minHeight  = an->height;
            ai->akashaNode = an->nextAkashaNode;
            goto getMinHeight_stub(context);
        }
    }

    ai->akashaNode = ai->akashaNode->nextAkashaNode;

    if (n->left != NULL) {
        left->height           = an->height+1;
        left->node             = node->left;
        left->nextAkashaNode   = ai->akashaNode;
        ai->akashaNode = left;
    }

    if (n->right != NULL) {
        right->height            = an->height+1;
        right->node              = node->right;
        right->nextAkashaNode    = ai->akashaNode;
        ai->akashaNode   = right;
    }

    goto getMinHeight_stub(context);
}
\end{lstlisting}
\caption{木の最も低い高さを取得する Code Segment}
\label{src:getMinHeight}
\end{figure}

% }}}

木をなぞるためのスタックに相当する \verb/AkashaNode/ を用いてノードを保持しつつ、高さを確認している。
スタックが空であれば全てのノードをなぞったので、次の処理へと \verb/goto/する。
空でなければ今なぞっているノードが葉であるか確認する。
葉ならば高さを更新し、スタックからノードを1つ破棄して自身に \verb/goto/する。
葉でなければ高さを1つ増やしながらスタックに左右の子供を積み、自身に \verb/goto/ する。

このように、Code Segment の検証に必要な仕様や処理は Meta Code Segment で記述することができる。
akasha におけるメタ計算を用いて、要素数13個まで任意の順で挿入を行なっても仕様が満たされることを検証した。
また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。

\section{CBMC を用いた赤黒木の検証}
同様に赤黒木の仕様をC言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて検証した。
CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。

比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文はCとは異なるために変換が必要である。
CbCはCと似た構文を持つため、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。

CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(図\ref{src:specificationCBMC}。
C では再帰呼び出しができるため、木の高さは再帰関数で確認している。
assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。

% {{{ CBMCにおける仕様記述

\begin{figure}[ht]
\begin{lstlisting}
void verifySpecification(struct Context* context,
                         struct Tree* tree) {
    assert(!(maxHeight(tree->root, 1) >
             2*minHeight(tree->root, 1)));
    return meta(context, EnumerateInputs);
}
\end{lstlisting}
\caption{CBMCにおける仕様記述}
\label{src:specificationCBMC}
\end{figure}

% }}}

挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(図\ref{src:enumerateInputs})。
検証する有限の要素数回分、ランダムな値を入力させることで挿入順の数え上げとする。

% {{{ CBMCによる挿入順の数え上げ

\begin{figure}[ht]
\begin{lstlisting}
void enumerateInputs(struct Context* context,
                     struct Node* node) {
    if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
        return meta(context, Exit);
    }

    node->key     = nondet_int();
    node->value   = node->key;
    context->next = VerifySpecification;
    context->loopCount++;

    return meta(context, Put);
}
\end{lstlisting}
\caption{CBMCによる挿入順の数え上げ}
\label{src:enumerateInputs}
\end{figure}

% }}}

CBMCでは有限のステップ数だけC言語を記号実行し、その範囲内で仕様が満たされるかを確認する。
条件分岐や繰り返しなどは展開されて実行される。
赤黒木検証時にCBMCが扱えた上限である 411 回まで展開を行なっても仕様は満たされていた。
しかし、赤黒木にバグを追加した際にも仕様の反例を得られず、411回の展開では赤黒木を正しく検証できないことも分かった。

よって、CBMCでは検証できない範囲の検証をakashaで行なえることが確認できた。

\section{考察と今後の課題}
CbC で記述したプログラムに対する仕様の検証を行なうことができた。
Code SegmentとData Segmentを用いてプログラミングすることで、検証用にコードを変更することなく検証を行なうことができた。

今回の検証では赤黒木が任意の順で有限の回数挿入されても木がバランスしていることを確認した。
挿入順は深さ優先探索で総あたりで探索しているため、赤黒木の操作に削除が含まれると上手く数え上げられない。
これは過去に探索した木の形状を記憶することで解決できる。
また、挿入を行なった後の木の高さを調べるために毎回木をなぞるため、木の要素数に比例した計算時間がかかっている。
各ノードに高さ情報を持たせ、木の操作時にノードの高さも更新することで高速に仕様をチェックすることができる。
ノードの高さ情報そのものの処理が正しいかといった、メタ計算の仕様も検証したい。
Meta Code Segment は任意の Code Segment に適用できるため、 akasha そのものの性質も akasha で検証できると考えている。
加えて、今回の検証に用いたメタ計算は赤黒木へのデータ構造に依存している部分が多い。
ポインタへの不正アクセス検出といった汎用的な検証機能をCBMCのように akasha にも追加していきたい。


\begin{thebibliography}{9}

\bibitem{cite:gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)
\bibitem{cite:rbtree} 小久保 翔平, 河野真治: Code Segment と Data Segment を持つ Gears OS の 設計 (2016)
\bibitem{cite:cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)
\bibitem{cite:dpp}  下地 篤樹, 河野 真治: 線形時相論理によるContinuation based Cプログラムの検証, 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), (2007)
\bibitem{cite:monad} Moggi, Eugenio: Notions of Computation and Monads, Inf. Comput (1991).
\bibitem{cite:cbmc} Clarke, Edmund and Kroening, Daniel and Lerda, Flavio: A Tool for Checking {ANSI-C} Programs, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)
\bibitem{cite:agda} \verb/The Agda Wiki - Agda/ \urlj{http://wiki.portal.chalmers.se/agda/pmwiki.php} \refdatej{2016-07-05}.
\bibitem{cite:nusmv} \verb/NuSMV home page/ \urlj{http://nusmv.fbk.eu/} \refdatej{2016-07-06}
\bibitem{cite:spin} \verb/Spin - Formal Verification/ \urlj{http://spinroot.com/spin/whatispin.html} \refdatej{2016-07-06}
\bibitem{cite:coq} \verb/Welcome! | The Coq Proof Assistant/ \urlj{https://coq.inria.fr/} \refdatej{2016-07-06}

\end{thebibliography}


\begin{biography}
\profile{n}{比嘉健太}{1992年生。2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。}
\profile{n}{河野真治}{1959年生。1984年3月東京工業大学理学部化学科卒業。1986年3月東京大学大学院情報工学課程修了。1989年5月工学博士。 1989-1996年 Sony Computer Science Laboratory, Inc. 1996年 琉球大学准教授。
情報処理学会, ACM , 日本ソフトウェア科学会各会員。
}
\end{biography}

\end{document}