\chapter{はじめに}
\label{chap:introduction}
\pagenumbering{arabic}

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

%% 想定外の挙動をしてほしくない


動作するプログラム(ソフトウェア)は高い信頼性を持つことが望ましい。

% しかし、既存の言語で関数より細かい単位に分割することは難しい。そのために当研究
% 室ではコードの単位を CodeGear ~
 プログラムの信頼性を保証するにはプログラムが期待される仕様を満たすことを検証する手法と、その仕様を直接証明する手法が存在している。

 
 % しかし、期待される仕様を満たすかを検証する際、仕様が大きくなるに連れ指数関数的に検証する項が増えてしまう。そのため、ここでは仕様を直接証明する手法を用いている。

そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している。

%% コードセグメントは通常の言語での関数を細かくしたものとしてよい？


本研究では CbC を用いて Tree、 Stack を実装し、等価な Agda の実装を使ってその仕
様の一部を証明した。


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

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

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

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

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

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

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

%\section{論文の構成}

%\section{Introduction}