\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 における型システムを部分型として定義する。
部分型を利用して CbC のプログラムが証明支援系言語 Agda 上で正しく証明可能な形で定義できることを示す。


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