\chapter{ソフトウェアの信頼性の保証}
\label{chap:introduction}
\pagenumbering{arabic}

% 序論の目安としては1枚半ぐらい．
% 英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも．



動作するソフトウェアは高い信頼性を持つことが望ましい。
そのためにはソフトウェアが期待される動作をすることを保証する必要がある。
期待される動作は仕様と呼ばれ、自然言語や論理によって記述される。

ソフトウェアの検証手法にはモデル検査と定理証明がある。
モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が正し
いことを確認する。モデル検査器には Spin\cite{spin} や、モデルを状態遷移系で記述
する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。

定理証明では。ソフトウェアが満たすべき仕様を論理式で記述し、その論理式が常に正し
いことを証明する。定理証明支援器には依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} などが存在する。

当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを記述する手法を提案している。
また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語としてCountinuation based C\cite{kaito:2015}を開発している。Continuation based C (CbC)はC言語と似た構文を持つ言語である。

本論文では Agda で
使ってその仕様の一部を証明した。


%% 動作するプログラムの信頼性を保証したい

%% そのために当研究室ではコードセグメント、データセグメントという単位を用いてプログラムを記述する手法を提案する

%% 処理の単位であるコードセグメントはメタ計算によって接続される

%% メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証することができる

%% 証明を使い、プログラムの信頼性を保証できるようにしたい

%%%
% やってること、やりたいことはAgdaとCbC言語で等価なプログラムを書き、証明すること
% Agdaではunblancedなbinary tree を作るとこまできた
% CbC側ではBalancedなredBlackTreeを作るところまではきている
%%%

% なんでAgda で証明するの ? Agda である理由は ?
% 他論文でも実装と異なる言語で証明している例は多い。
% もともとの言語が証明支援ではない。関数型言語(証明支援系言語)でのプログラミングは手続き型のプログラミングと異なる

%\section{論文の構成}

%\section{Introduction}