\chapter{CbC とメタ計算としての検証手法}
ソフトウェアの規模が大きくなるにつれてバグは発生しやすくなる。
バグとはソフトウェアが期待される動作以外の動作をすることである。
ここで期待された動作は仕様と呼ばれ、自然言語や論理によって記述される。
検証とは定められた環境下においてソフトウェアが仕様を満たすことを保証することである。

ソフトウェアの検証手法にはモデル検査と定理証明がある。

モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認することである。
モデル検査器には、 Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
定理証明を行なうことができる言語には、依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。

モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。
言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。
検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードは検証のコードとは別の言語であったり、既存の実装に対する検証は行なえないなどの問題がある。
そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。

Continuation based C (CbC)はC言語と似た構文を持つ言語である。
CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。
CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。
CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。
検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。

本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha~\cite{atton-ipsjpro} を用いて仕様を検査する。
また、定理証明的な検証として、 CbC のプログラムを証明支援系言語 Agda 上で証明する。
Agda で CbC の項を表現するために部分型を用いてCbCを型付けし、Agdaでの定義からCbCの形式的な定義を得る。
そして、Agda 上で Single Linked Stack の性質の証明を行なう。


\section{本論文の構成}
本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算の例として GearsOS の解説を行なう。
第\ref{chapter:akasha}章にて GearsOS 上の非破壊赤黒木の検証をメタ計算ライブラリ akasha にて行なう。
次に第\ref{chapter:type}章で型システムについて取り上げる。
型システムの定義と CbC の型システムの定義に必要な単純型、レコード型、部分型について述べる。
第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。
Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。
第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。