\documentclass[techrep]{ipsjpapers}
\usepackage[dvipdfmx]{graphicx}
\usepackage{url}
\usepackage{listings,jlisting}
\usepackage{enumitem}
\usepackage{bussproofs}
\usepackage{amsmath}
\usepackage{multirow}
\usepackage{here}
\usepackage{cite}
\usepackage{listings}
\usepackage{amssymb}

\lstset{
    language=C, 
    tabsize=2, 
    frame=single, 
    basicstyle={\ttfamily\footnotesize},% 
    identifierstyle={\footnotesize},% 
    commentstyle={\footnotesize\itshape},% 
    keywordstyle={\footnotesize\bfseries},% 
    ndkeywordstyle={\footnotesize},% 
    stringstyle={\footnotesize\ttfamily}, 
    breaklines=true, 
    captionpos=b, 
    columns=[l]{fullflexible},% 
    xrightmargin=0zw,% 
    xleftmargin=1zw,% 
    aboveskip=1zw, 
    numberstyle={\scriptsize},% 
    stepnumber=1, 
    numbersep=0.5zw,% 
    lineskip=-0.5ex, 
}
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small,tt}}

\input{dummy.tex} %% Font 

% ユーザが定義したマクロなど．
\makeatletter

\begin{document}

% 和文表題
\title{GearsOS の Agda による記述と検証}
% 英文表題
\etitle{}

% 所属ラベルの定義
\affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
\affilabel{2}{琉球大学工学部情報工学科\\Information Engineering, University of the Ryukyus.}

% 和文著者名
\author{
  外間 政尊\affiref{1}
  \and
  河野 真治\affiref{2}
}

% 英文著者名
\eauthor{
  Masataka HOKAMA\affiref{1}
  \and
  Shinji KONO\affiref{2}
}

% 連絡先（投稿時に必要．製版用では無視される．）
\contact{外間 政尊\\
        〒903-0213 沖縄県西原町千原1番地\\
	琉球大学工学部情報工学科\\
        TEL: (098)895-2221\qquad FAX: (098)895-8727\\
        email: masataka@cr.ie.u-ryukyu.ac.jp}

% 和文概要
\begin{abstract}
    Gears OS は継続を主とするプログラミング言語 CbC で記述されている。 OS やアプリケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。 確認方法にはモデル検査と証明がある。 ここでは定理証明支援系Agdaを用いた、CbC 言語の証明方法を考える。 CbC は関数呼び出しを用いず goto 文により遷移する。 これを継続を用いた関数型プログラムとして記述することができる。 この記述はAgda上で決まった形を持つ関数として表すことができる。 Gears OS のモジュールシステムは、実装とAPI を分離することを可能にしている。 このモジュールシステムを Agda 上で記述することができた。 継続は不定の型を返す関数で表されるので、継続に直接要求仕様を Agda の論理式として渡すことができる。 継続には仕様以外にも関数を呼び出すときの前提条件(pre-condition)を追加することが可能である。 これにより、Hoare Logic 的な証明を Agda で記述した CbC に直接載せることが可能になる。 Agda で記述された CbC と実装に用いる CbC は並行した形で存在する。 つまり、CbC のモジュールシステムで記述されたプログラムを比較的機械的に Agda で記述された CbC 変換することができる。 本論文ではAgda 上での CbC の記述手法とその上での Hoare Logic 的な証明手法について考察する。
\end{abstract}

% 英文概要
\begin{eabstract}
\end{eabstract}

% 表題などの出力
\maketitle

% 本文はここから始まる

% Introduce
% Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。

% 研究目的

% 信頼性の高いOS

\section{ソフトウェアの信頼性の保証}

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

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

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

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

本論文では CbC で Interface と呼ばれる記述方法を Agda で表現し、その記述を通した
実装の仕様の一部に対して証明を行なった。

\section{CodeGear, DataGear}

CodeGear、 DataGear は当研究室で提案している検証の単位である。
処理の単位を CodeGear、処理に使うデータの単位を DataGear とし、
CodeGear を他の CodeGear と継続することでプログラムを構成する。
図\ref{fig:csds}のように Input DataGear を受け取り、 CodeGear で Output
DataGear に変更を加えることでプログラムを記述していく。
% CS,DSの図
\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.25}{\includegraphics{pic/csds.pdf}}
 \end{center}
 \caption{CodeGear と DataGear}
 \label{fig:csds}
\end{figure}


\section{ CbC での CodeGear、 DataGear}
CbC での簡単な記述例をソースコード\ref{code_simple}、流れを図\ref{fig:code_simple}に示
す。CbC では CodeGear を$\_\_$code キーワードを指定する。その際、Input 
DataGear は関数の引数として定義される。 CodeGear は継続で次の CodeGear
に遷移するために関数末尾で goto キーワードの後に CodeGear 名と Input 
DataGear を指定する必要がある。

ソースコード\ref{code_simple}では　cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、
cs1 の Input DataGear である。

\begin{lstlisting}[frame=lrbt,label=code_simple,caption={CodeGear の継続の例}]
__code cg0(int a, int b){
  goto cg1(a+b);
}

__code cg1(int c){
  goto cg2(c);
}
\end{lstlisting}


\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.6}{\includegraphics{pic/codesegment.pdf}}
 \end{center}
 \caption{ソースコード\ref{code_simple}の流れ}
 \label{fig:code_simple}
\end{figure}

CbC の継続は、呼び出し元の情報を持たずに処理を続ける。この継続を軽量継続と呼ぶ。
ソースコード\ref{code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継
続に指定された CodeGear へ継続する。

CbC でのループ処理の記述例をソースコード\ref{factorial}、流れを図\ref{fig:factorial}に示
す。
軽量継続では関数呼び出しのスタックは存在しないが、ソースコード\ref{factorial}の
ように計算中の値を DataGear で持つことでループ処理を行なうこともできる。

\begin{lstlisting}[frame=lrbt,label=factorial,caption={階乗を求め
る CbC プログラムの例}]
__code print_factorial(int prod)
{
  printf("factorial = %d\n",prod);
  exit(0);
}

__code factorial0(int prod, int x)
{
  if ( x >= 1) {
    goto factorial0(prod*x, x-1);
  }else{
    goto print_factorial(prod);
  }
  
}

__code factorial(int x)
{
  goto factorial0(1, x);
}

int main(int argc, char **argv)
{
  int i;
  i = atoi(argv[1]);
  
  goto factorial(i);
}
\end{lstlisting}

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.6}{\includegraphics{pic/factorial.pdf}}
 \end{center}
 \caption{階乗を求める CbC プログラムの流れ}
 \label{fig:factorial}
\end{figure}

\section{メタ計算}
% メタ計算の論文引用どうするかな…
% メタプログラミング~系の本とかもいれていいのかな

メタ計算(リフレクション)とは、対象とするレベルとメタなレベルを分離し、対象レベルでの推論や計算に
関するメタな情報をメタレベルで明示的に記述し操作する。

メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理
と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管
理やスレッド管理、資源管理等の計算がこれに当たる。



% \section{Meta CodeGear とMeta DataGear}

% CbC 


% \section{Interface}

% Interface では使用する DataGear とそれに対する処理を行う CodeGear の集合をま
% とめて定義する。

% \lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの記述] {src/interface.cbc}

% DataGear に対して何らかの操作(API)を行う CodeGear とその
% CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
% として定義される。

% Interface を記述することでデータ構造の api と DataGear の結びつきを高め、呼び出しが容易になる。


\section{Context}
CbC で DataGear を扱う際、 Context と呼ばれる接続可能な CodeGear、 DataGear のリ
スト、Temporal DataGear のためのメモリ空間等を持っている Meta DataGearである。
CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必
要がある。

\section{stub CodeGear}
CodeGear が必要とする DataGear を取り出す際、 Context を通す必要がある。
しかし、 Context を直接扱えるようにするのは信頼性を損なう。そのため CbC では
Context を通して必要なデータを取り出して次の Code Gear に接続する stub CodeGear
を定義している。CodeGear は stub CodeGear を介してのみ必要な DataGear へアクセス
することができる。 stub CodeGear は CodeGear 毎に生成され、次の CodeGear へと接
続される。
stub CodeGear は CodeGear の Meta CodeGear に当たる。


\section{CbCによる Interface の記述と継続}

CodeGear は通常の関数と比べ、細かく分割されるためメタ計算をより柔軟に記述でき
る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear
、 Meta DataGear が存在する。

CbC で実装していくうちに、stub CodeGear の記述が煩雑になることが分かった。
そのため 既存の実装を モジュールとして扱うため Interface を導入した。

Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
として定義される。

例として CbC による Stack Interface \ref{interface-define},
\ref{interface}がある。Stack への push 操作に注目すると、
実態は SingleLinkedStack の push であることが\ref{interface}で分
かる。実際の SingleLinkedStack の push では Stack を指定する必要があるが、
Interface で実装した Stack では push 先の Stack が stackImpl として扱
われている。この stackImpl は$ Stack->push $で呼ばれた時の Stack と同じになる。
これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。

このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
しが容易になる。

\lstinputlisting[label=interface-define, caption=CbCでのStack-Interfaceの定義] {src/interface.cbc}

\lstinputlisting[label=interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc}

\section{定理証明支援器 Agda での証明}

型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
。
型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。

\section{Agda の文法}

Agda はインデントに意味を持つため、きちんと揃える必要がある。
また、スペースの有無は厳格にチェックされる。
なお、 \verb/--/ の後はコメントである。

Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ
ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。

通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。
また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。
モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードの後に
関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠
す場合は \verb/hiding/ キーワードを用いる。
なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/opestack に対する操作を定義しており、n/ キーワードを使うことで展開できる。
モジュールをインポートする例をリスト~\ref{agda-import}に示す。

\lstinputlisting[label=agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda}

Agda における型指定は $:$ を用いて行う。

例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。

データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
\verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
例えば Bool 型を定義するとリスト~\ref{agda-bool}のようになる。
Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。
Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く。

\lstinputlisting[label=agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}

関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書
ける。
また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
時の型は \verb/A -> (A -> B)/のように考えられる。
Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{agda-function}のようになる。

\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda}

引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{agda-not}のようになる。

\lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}

パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。
なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。

\lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}

Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
\verb/\arg1 arg2 -> function body/ のように書くことができる。
例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。
関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。

\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}

Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{agda-where} のように書ける。
これは \verb/f'/ と同様の動作をする。
\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}

データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{agda-nat})。
自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。

\lstinputlisting[label=agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}

自然数に対する演算は再帰関数として定義できる。
例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{agda-plus}のように書ける。

この二項演算子は中置関数として振る舞う。
前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくと、関数を呼ぶ
時にあたかも前置や後置演算子のように振る舞うことができる。
例えば \verb/!_/ を定義すると \verb/! true/ のように利用でき、\verb/_~/ を定義すると \verb/false ~/ のように利用できる。

また、Agda は再帰関数が停止するかを判別できる。
この加算の二項演算子は左側がゼロに対しては明らかに停止する。
左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。

\lstinputlisting[label=agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}

次に依存型について見ていく。
依存型で最も基本的なものは関数型である。
依存型を利用した関数は引数の型に依存して返す型を決定できる。
なお、依存型の解決はモジュールのインポート時に行なわれる。

Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つ x を受け取り、Bを返す。
ここで B の中で x を扱っても良い。
例えば任意の型に対する恒等関数はリスト~\ref{agda-id}のように書ける。

\lstinputlisting[label=agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}

この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。

多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
Agda はこのような推論をサポートしており、推論可能な引数は省略できる。
推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、変数を
\verb/{}/ でくくることで表す。

例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{agda-implicit-id}のようになる。
この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。

\lstinputlisting[label=agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}

Agda のデータには C における構造体に相当するレコード型も存在する。
定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{agda-record}のようになる。
レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
複数の値を列挙する際は \verb/;/ で区切る。

\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}

構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。
なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。
レコード内の値は \verb/record oldRecord {field = value ; ... }/ という構文を利用し更新することができる。
Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。

\lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}


% \section{Natural Deduction}
% % Natural Deduction のお話。細かい規則は…書かなきゃいけないよね…
% % いらない規則は省略しようと、少なくとも3段論法を証明できるだけ置く。。。？
% % とりあえず証明に使えるやつは全部書いて必要あるやつを詳しく。

% Natural Deduction (自然演繹)は Gentzen によって作られた論理及びその証明システムである。
% % ~\cite{Girard:1989:PT:64805}。
% 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。

% Natural Deduction では次のように

% \begin{eqnarray}
%     \vdots \\ \nonumber
%     A \\ \nonumber
% \end{eqnarray}

% と書いた時、命題Aを証明したことを意味する。証明は木構造で表わされ、葉の命題は仮
% 定となる。

% \begin{eqnarray}
%     \label{exp:a_implies_b}
%     A \\ \nonumber
%     \vdots \\ \nonumber
%     B \\ \nonumber
% \end{eqnarray}

% 式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。
% この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。

% ここで、推論規則により記号 $ \Rightarrow $ を導入する。

% \begin{prooftree}
%     \AxiomC{[$ A $]}
%     \noLine
%     \UnaryInfC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ B $ }
%     \RightLabel{ $ \Rightarrow \mathcal{I} $}
%     \UnaryInfC{$ A \Rightarrow B $}
% \end{prooftree}

% $ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
% A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
% このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
% なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。

% alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
% それを踏まえ、 natural deduction には以下のような規則が存在する。

% \begin{itemize}
%     \item Hypothesis

%         仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。

%         $ A $

%     \item Introductions

%         導入。証明された論理式に対して記号を導入することで新たな証明を導く。


% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A $ }
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ B $ }
%     \RightLabel{ $ \land \mathcal{I} $}
%     \BinaryInfC{$ A \land B $}
%   \end{prooftree}

% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A $ }
%     \RightLabel{ $ \lor 1 \mathcal{I} $}
%     \UnaryInfC{$ A \lor B $}
%   \end{prooftree}

% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ B $ }
%     \RightLabel{ $ \lor 2 \mathcal{I} $}
%     \UnaryInfC{$ A \lor B $}
%   \end{prooftree}

% \begin{prooftree}
%     \AxiomC{[$ A $]}
%     \noLine
%     \UnaryInfC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ B $ }
%     \RightLabel{ $ \Rightarrow \mathcal{I} $}
%     \UnaryInfC{$ A \Rightarrow B $}
%   \end{prooftree}

% \item Eliminations

%     除去。ある論理記号で構成された証明から別の証明を導く。

% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A \land B $ }
%     \RightLabel{ $ \land 1 \mathcal{E} $}
%     \UnaryInfC{$ A $}
%   \end{prooftree}

% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A \land B $ }
%     \RightLabel{ $ \land 2 \mathcal{E} $}
%     \UnaryInfC{$ B $}
%   \end{prooftree}

% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A \lor B $ }

%     \AxiomC{[$A$]}
%     \noLine
%     \UnaryInfC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ C $ }

%     \AxiomC{[$B$]}
%     \noLine
%     \UnaryInfC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ C $ }

%     \RightLabel{ $ \lor \mathcal{E} $}
%     \TrinaryInfC{ $ C $ }
%   \end{prooftree}

% \begin{prooftree}
%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A $ }

%     \AxiomC{ $ \vdots $}
%     \noLine
%     \UnaryInfC{ $ A \Rightarrow B $ }

%     \RightLabel{ $ \Rightarrow \mathcal{E} $}
%     \BinaryInfC{$ B $}
%   \end{prooftree}
  
% \end{itemize}

% 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
% natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。

% それぞれの記号は以下のような意味を持つ
% \begin{itemize}
%     \item $ \land $
%         conjunction。2つの命題が成り立つことを示す。
%         $ A \land B $ と記述すると、 A かつ B と考えることができる。

%     \item $ \lor $
%         disjunction。2つの命題のうちどちらかが成り立つことを示す。
%         $ A \lor B $ と記述すると、 A または B と考えることができる。

%     \item $ \Rightarrow $
%         implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
%         $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。
% \end{itemize}

% Natural Deduction では、これまでで説明したような規則を使い証明を行うことができる。

% 例として Natural Deduction で三段論法の証明を行う。
% このとき、「A は B であり、 B は C である。よって A は C である」 が証明するべき
% 命題である。

% この命題では 「A は B であり」と 「B は C である」の二つの小さい命題に分けられる。
% この「A は B であり」から、AからBが導出できることが分かり、これは $ A \Rightarrow B $ と表せる。
% また、「B は C である」から、BからCが導出できることが分かる。これも「A は B であ
% り」の時と同様に $ B \Rightarrow C $ と表せる。


% \begin{prooftree}
%     \AxiomC{ $ [A] $ $_{(1)}$}
%     \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
%     \RightLabel{ $ \land 1 \mathcal{E} $ }
%     \UnaryInfC{ $ (A \Rightarrow B) $ }
%     \RightLabel{ $ \Rightarrow \mathcal{E} $}
%     \BinaryInfC{ $ B $ }

%     \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
%     \RightLabel{ $ \land 2 \mathcal{E} $ }
%     \UnaryInfC{ $ (B \Rightarrow C) $ }

%     \RightLabel{ $ \Rightarrow \mathcal{E} $}
%     \BinaryInfC{ $ C $ }
%     \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
%     \UnaryInfC{ $ A \Rightarrow C $}
%     \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
%     \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
% \end{prooftree}


% Natural Deductionでは次のような証明木になる。


% \begin{figure}[htpb]
%    \begin{center}
%      \scalebox{0.25}{\includegraphics{pic/modus-ponens.pdf}}
%    \end{center}
%    \caption{自然演繹での三段論法の証明}
%    \label{fig:modus-ponens}
% \end{figure}

% これにより自然演繹を使って三段論法が証明できた。
% %%%%%%%%%%%%%%%%%%%%%%


% \section{Natural Deduction と 型付き $ \lambda $  計算}

% ここでは、 Natural Deduction と型付き$ \lambda $ 計算の対応を定義する。
% 対応は以下の表\ref{table:curry-howard}のようになる。

% \begin{center}
%   \begin{table}[h]
%     \scalebox{0.5}{
%       \begin{tabular}{|c|c|} \hline
%         Natural Deduction           & 型付き $ \lambda $ 計算  \\ \hline \hline
%         $ A $                       & 型 A を持つ変数 x \\ \hline
%         $ A \Rightarrow B $         & 型 A を取り型 B の変数を返す関数 f \\ \hline
%         $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline
%         $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline
%         $ A \land B $               & 型 A と型 B の直積型 を持つ変数 x \\ \hline
%         $ \land \mathcal{I} $       & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline
%         $ \land 1 \mathcal{E} $     & 直積型からの型Aを取り出す射影fst \\ \hline
%         $ \land 2 \mathcal{E} $     & 直積型からの型Bを取り出す射影snd \\ \hline
%       \end{tabular}
%     }
%     \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
%     \label{table:curry-howard}
%   \end{table}
% \end{center}

% この対応をもとに Agda で型付き $\lambda$ 計算による証明を示す。
% % ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。
% ここでも先程 Natural Deduction で証明した三段論法を例とする。
% % この三段論法は自然演繹では\ref{fig:modus-ponens}のようになっていた。

% % \begin{figure}[htpb]
% %    \begin{center}
% %        \includegraphics{pic/modus-ponens.pdf}
% %    \end{center}
% %    \caption{自然演繹での三段論法の証明}
% %    \label{fig:modus-ponens}
% % \end{figure}

% %McCこの証明木に対応するAgdaによる証明はリスト\ref{agda-moduse-ponens}のようになる。

% \begin{lstlisting}[frame=lrbt,label=agda-moduse-ponens,caption={ Agda による
%     三段論法の定義と証明}]    
% data _×_ (A B : Set) : Set where
%   <_,_> : A → B → A × B

% fst : {A B : Set} → A × B → A
% fst < a , _ > = a

% snd : {A B : Set} → A × B → B
% snd < _ , b > = b 


% f : {A B C : Set} → ((A → B) × (B → C)) → (A → C)
% f = λ p x → (snd p) ((fst p) x)
% \end{lstlisting}

% 自然演繹での三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。

% ここで $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
% よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
% これをラムダ式で書くとリスト~\ref{agda-modus-ponens}のようになる。
% 仮定 $ (A \rightarrow B) \times (B \rightarrow C) $  と仮定 A から A $ \rightarrow $ C を導いている。

% 仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。
% fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。
% もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。
% 得られた B を snd p に適用することで最終的に C が導ける。

% \lstinputlisting[label=agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda}

% このように Agda でも自然演繹と同様に証明を記述できる。

\section{Agda での CodeGear 、 DataGear 、 継続の表現}
Agda と CbC を対応して CodeGear、 DataGear、 継続を Agda で表現する。
また、 Agda で継続を記述することで得た知見を示す。

DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義
していく。記述は~\ref{agda-ds}のようになる。

\lstinputlisting[label=agda-ds, caption=Agda における DataGear の定義]
{src/DataSegment.agda}

CodeGear は DataGear を受け取って DataGear を返すという定義であるため、
$ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{agda-cs})を定義する。

\lstinputlisting[label=agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda}

CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの
と対応する。

CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す
ることに相当する。

CbC での軽量継続は

\begin{itemize}
 \item 次に実行する CodeGear を指定する
 \item CodeGear に渡す DataGear を指定する
 \item 現在実行している CodeGear から制御を指定された CodeGear へと移す
\end{itemize}

の機能を持っている。

この機能を満たす関数はソースコード\ref{agda-goto} として定義されている。

\lstinputlisting[label=agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}

goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する
CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。


\section{Agda での Stack、 Tree の実装}

ここでは Agda での Stack 、 Tree の実装を示す。

Stack の実装を以下のソースコード\ref{stack-impl}で示す。
実装は SingleLinkedStack という名前で定義されている。
定義されている API は push を例に残りは省略する。残りのの実装は付録に示す。 %~\

\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装] {src/AgdaStackImpl.agda}


Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
Maybe 型では値が存在する場合は Just 、 存在しない場合は　Nothing を返す。

SingleLinkedStack 型では、この Element の top 部分のみを定義している。

Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum
の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい
stack を返すというような実装をしている。

Tree の実装(以下のソースコード\ref{tree-impl})は RedBlackTree という名前で定義されている。
定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\

\lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda}

Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。
Tree を構成する末端の Node は leafNode 型で定義されている。

RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの
Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。

Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け
取り、Tree の root に Node が存在しているかどうかで場合分けしている。
Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け
取ったキーと値を新しいノードとして追加する。
Just が返ってきたときは root が存在するので、経路情報を積むために nodeStack を初
期化し、受け取ったキーと値で新たなノードを作成した後、ノードが追加されるべき位置
までキーの値を比べて新しい Tree を返すというような実装になっている。

\section{Agda における Interface の実装}

%% 書くこと
% stack の Interface部分と redBlackTree の Interface部分。
% interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい

Agda 側でも CbC 側と同様に interface を実装した。
interface は record で列挙し、ソースコード~\ref{agda-interface}のように紐付けることができる。
CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。

例として Agda で実装した Stack 上の interface (ソースコード\ref{agda-interface})を見る。
Stack の実装は SingleLinkedStack(ソースコード\ref{agda-single-linked-stack}) として書かれている。それを Stack 側から
interface を通して呼び出している。

ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
実際に使われる Stack の操作は StackMethods にある push や popである。この push
や pop は SingleLinkedStack で実装されている。

% \lstinputlisting[label=agda-single-linked-stack, caption=Agda における Stack
% の実装] {src/AgdaSingleLinkedStack.agda}

\lstinputlisting[label=agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda}

interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取
り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更
して継続を返す型に変わっている。

また、 Tree でも interface を記述した。

\lstinputlisting[label=agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda}

interface を記述することによって、データを push する際に予め決まっている引数を省
略することができた。
また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確
化された。

% 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push
% する可能性があったが、 pushStack では紐付けた Stack に push することになり

\section{継続を使った Agda における Test , Debug}

Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず
しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動
作をしているかを確認するために行なった手法を幾つか示す。

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
今回は実験中にソースコード\ref{agda-stack-test}のような Test を書いた。
この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー
タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。

\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda}

上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる
ため 05 が refl でコンパイルが通るようになる。
今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。
032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確
実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、
かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って
いるかを確認している。

この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分
かる。


また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
とができた。

ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること
ができる。
% \ref{sintax}のようなコードを
% \begin{lstlisting}[frame=lrbt,label=sintax,caption={ 通常の継続の
%     コード}]

% \end{lstlisting}

% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={ 糖衣構文
%     を用いた継続のコード}]

% \end{lstlisting}

ソースコード~\ref{agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n
(Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。
また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ
とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。

 \lstinputlisting[label=agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda}

今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ
とが分かった。


%getRedBlackTree の関数に
% \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda}
% Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう


\section{Agda による Interface 部分を含めた Stack の部分的な証明}
\label{agda-interface-stack}

% Stack の仕様記述
Stack や Tree の Interface を使い、 Agda で Interface を 経由した証明が可能であ
ることを示す。
ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。

Stack の処理として様々な性質が存在する。例えば、

\begin{itemize}
 \item Stack に push した値は存在する
 \item Stack に push した値は取り出すことができる
 \item Stack に push した値を pop した時、その値は Stack から消える
 \item どのような状態の Stack に値を push しても中に入っているデータの順序は変わらない
 \item どのような状態の Stack でも、値を push した後 pop した値は直前に入れた値と一致する
\end{itemize}

などの性質がある。

ここでは「どのような状態の Stack でも、値を push した後 pop した値は直前
に入れた値と一致する」という性質を証明する。

まず始めに不定状態の Stack を定義する。ソースコード~\ref{agda-in-some-state}
の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー
ド~\ref{agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を
2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明す
る。

 \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}
 
この証明では stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
型に書かれている。

この関数本体で返ってくる値は$ x \equiv x1 と y \equiv y1$　のため record でまと
めて refl で推論が通る。
これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
のを受け取れることが証明できた。


% \lstinputlisting[label=agda-Test, caption=]{src/AgdaStackTest.agda}

\section{Agda による Interface 部分を含めた Binary Tree の部分的な証明と課題}
ここでは Binary Tree の性質の一部に対して証明を行う。
Binary Tree の性質として挙げられるのは次のようなものである
% 上の２つはデータ構造として最低限守られるべき部分ではあるがとりあえず書いてる

\begin{itemize}
 \item Tree に対して Node を Put することができる。
 \item Tree に Put された Node は Delete されるまでなくならない。
 \item Tree に 存在する Node とその子の関係は必ず「右の子 $>$ Node」かつ「Node $>$ 左の子」の関係になっている。
 \item どのような状態の Tree に値を put しても Node と子の関係は保たれる
 \item どのような状態の Tree でも値を Put した後、その値を Get すると値が取れる。
\end{itemize}

ここで証明する性質は

${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。

\lstinputlisting[label=agda-tree-proof, caption=Tree Interface の証
明]{src/AgdaTreeProof.agda}

この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree
に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの
である。

しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した
Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、
key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が
あった。今回この証明では Put した Node と Get した
Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合
同であることを示すことが困難であった。

今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を
行おうと考えている。

\section{Hoare Logic}
\label{hoare-logic}

Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}[0.3]{\includegraphics{pic/hoare-logic.pdf}}
 \end{center}
 \caption{hoare logicの流れ}
 \label{fig:hoare}
\end{figure}


このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
動きをすることを証明することができる。

この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
\ref{fig:cbc-hoare} のように表せるのではないか考えている。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}[0.3]{\includegraphics{pic/cbc-hoare.pdf}}
 \end{center}
 \caption{cbc と hoare logic}
 \label{fig:cbc-hoare}
\end{figure}

この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
Pre Condition が CodeGear に入力として与えられる Input DataGear、Command が
CodeGear、 Post Condition を Output DataGear として当てはめることができると考えて
いる。

今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に
当てはめ、幾つかの実装を証明していく。

% Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
% 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
%%
% 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
% 入した。
%%

\nocite{*}
\bibliographystyle{ipsjunsrt}
\bibliography{sigos}

\end{document}