\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvipdfmx]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
%\pagestyle{fancy}
%\usepackage{abstract}
\usepackage{url}
\usepackage{bussproofs}
\usepackage{listings,jlisting}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}

\lstset{
  frame=single,
  keepspaces=true,
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}


\input{dummy.tex}
%\renewcommand{\abstractname}{Abstract}
\begin{document}
\title{CbC言語によるプログラムの検証}
\author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
\date{}
\maketitle
\thispagestyle{fancy}

\section{研究目的}

%% Agdaのお勉強のこと、CbCをAgdaに直したこと、CbC側のDeletionのこと

%% CbC でソフトウェアを検証できるかを CbCで書いた RBTree と Agda で同様に書いた RBTree を検証することで示す

%% ソフトウェアの規模が大きくなるにつれて期待されない動作をすることが増える。ここでは期待される動作を仕様、期待されない動作をバグと呼ぶことにする。
%% それにはソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。
%% 期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。

%% 特に実際に動作するソフトウェアを検証、証明できることが望ましい。
%% そのために当研究室では CodeSegment 、 Data Segment という単位を用いてソフトウェアを記述する手法を提案している。
%% 処理の単位である CodeSegment は、メタ計算によって相互に接続される。
%% メタ計算を切り替えることで CodeSegment を変更することなくソフトウェアの性質を検証することができる。
% CbC検証と実装が同一の言語で行える言語である。
% CbCの特徴はだいじょうぶ？完全じゃなくていいけどある程度は乗せなきゃ駄目だよね

ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証する方法として代表的なものはモデル検査と、定理証明が存在している。
モデル検査はソフトウェアの状態をすべて数え上げ、すべての状態で仕様が正しいことを確認する方法である。
定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明することである。%% atton-master papar より
%% モデル検査や、証明でソフトウェアを検証する際、検証に使われる言語と実装に使う言語が異なるという問題がある。
%% そのため、二重で同じソフトウェアを記述する必要があるうえ、検証に用いるソースコードは状態が遷移する形で記述する必要があるなど実装されているコードに比べて記述が困難である。
%% 検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードが検証のコードと別の言語であったり、既存の実際に対する検証は行えないなどの問題がある。

% この問題を解決する為に
当研究室では検証と実装を同一の言語で行える Continuation based C ( CbC )言語を開発している。
本研究では、検証や証明に直接使用できる言語として CbC を用いる。

 %% CbC 上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法は、比嘉(2016)\cite{Yasutaka:2016}により提案、実装されている。
%% また、赤黒木の仕様が、限定的な木の大きさの範囲内で検証されている。

%% 木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。

%% プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。

%% 部分型を用いて CbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。

本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検証、証明する。

%%検証と証明の話書かないとAgda出せなくない？

\section{Countinuation based C (CbC)}
Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。
CbC では OS や組み込みソフトウェアを主な対象としている。
CbC は C 言語とほぼおなじ構文を持ち、よりアセンブラに近い形でプログラムを記述する。

CbC では C の関数の代わりに CodeSegment を用いて処理を記述する。
CodeSegment は値を入力として受取り、出力を行う処理の単位で、それらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。
CbC の CodeSegment を定義するには C とは少し異なり関数定義のの先頭に \_\_code が付く。
DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。CodeSegment の入力となる DataSegment は Input DataSegment　出力 を Input DataSegment は関数の引数として定義する。次の CodeSegment に処理を移す際は、 goto の後に CodeSegment 名と Input DataDataSegment を指定する。
% 図\ref{fig:CSContinuation}は CodeSegment 感の処理の流れを表している。

%%% figure
%% \begin{figure}[htbp]
%%    \begin{center}
%%        \includegraphics[width=60mm]{../pic/codesegment.pdf}
%%    \end{center}
%%    \caption{ goto による CodeSegment 間の接続}
%%    \label{fig:CSContinuation}
%% \end{figure}

CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。
例として CbC による Stack に対する操作のコード示す。

\newpage
\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace}

このコードでは Stack に対する push と pop を定義している。

push や pop は必要があるときに外から呼ばれる。

push では element で新しい要素を作って、次の要素との関係、 push する要素を入れ、Stack の top を書き換えて次のCodeSegmentに飛ぶ。

pop では Stack の top に data があればその data を next に入れ、次のCodeSegmentに飛ぶ。 top に data が無ければ NULL を next の Input Data に入れて次のCodeSegmentに飛ぶ。

%% また CbC で Functional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。

比嘉(2016)\cite{Yasutaka:2016}では CbC における CodeSegment 、 DataSegment が部分型で定義できることが示されている。
これより、 CbC で Functional に書かれたプログラムは等価な Agda のコードの置き換えることができる。
本研究では CbC の代わりに等価なAgdaのコードに変換することで証明を行う。

\section{Agda}
Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。
依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。

CbC を Agda に変換する場合 DataSegment をレコード型、 CodeSegment は関数型となる。

前項で示した CbC で書かれた Stack の操作をAgda に変換したコードを示す。

\lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace}

%CbC で書かれた Stack の CodeSegment が要素、Tree、

Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。関数の型では → または \verb/->/ を使い定義する。
%% 引数は変数で受けることもできるが、具体的な型構築子を渡された時の挙動を定義することができる。これはパターンマッチと呼ばれ、型構築子で case 文を行っているようなものである。
%% パターンマッチはすべての場合を含む必要があり、特定のものだけ異なる挙動にしたい場合は構築子を幾つか指定した後に変数で受けることで解決できる。なお、マッチした値を変数として利用しない場合は _ で値を捨てることもできる。

関数にはリテラルが存在し、関数を定義せずにその場で値を生成することもできる。これは ラムダ式と呼ばれ、 \verb/\arg1 arg2 -> function body/ または $ \lambda $ arg1 arg2 → function body のように記述できる。上の例では pushStack の \verb/\s1 -> next (record {stack = s1})/ や、 popStack の \verb/\s1 -> next s0/ が ラムダ式である。


%%%%%%%%
 Agda のレコード型も存在する。定義をする際は record キーワードのあとにレコード名、型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコードを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙していく。複数の値を列挙する際は ; で区切る。上の例では \verb/record {stack = s1}/ がそれにあたる。



%% リテラル is 何


%% このコードでは push 、 pop の関数を定義をしている。
%% push では要素を追加した新しいStackを返す。
%% pop では data があればそのデータを pop し、しない場合はそもそも

このように CbC のコードを Agda に変換し、証明を行う。


% 証明を行う前に自然演繹について説明
%% 自然演繹とは Gentzen によって作られた論理とその証明システムである。命題変数と記号を用いた論理式で論理を記述し、推論規則を使って変形することで求める論理式を導く。

%% 始めに、自然演繹と型付き$ \lambda $ 計算の対応を定義する。
%% \begin{center}
%% \begin{table}[htbp]
%% \scalebox{0.75}{
%% \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}
%% \end{table}
%% \end{center}

%% ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。

%% この三段論法を自然演繹による証明木にすると次のようになる。

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


%% この証明木に対応するAgdaによる証明は次のようになる。

%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single]
%% 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{src: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=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced}

%% このように Agda では証明を記述することができる。

% Agdaの知識ってどう出す？

%TODO 定理証明とプログラムの話

%% \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}


%% Agdaによる三段論法の証明

%% 定理証明支援器では Curry-Howard 同型対応により書いた命題通りに書いたプログラムをコンパイルが通ることはその命題を証明することが等しい。

%% 以下に CbC で書かれた Stack の 定義の一部と それを Agda に変換したものの定義の一部分を示す。
%% push だけじゃなく pop も入れたほうがいい…のかな

%%% CbCのCodeSegmentの例

%% context.h


%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single]
%% \end{lstlisting}

  % Stack.agdaのコード
%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single]
%% record Stack {a t : Set} (stackImpl : Set) : Set  where
%%   field
%%     stack : stackImpl
%%     push  : stackImpl -> a -> (stackImpl -> t) -> t

%%     pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t
%%     pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} ))
%% \end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{RedBlackTree}
RedBlackTree とは拡張された二分探索木で、木のバランスを取るための情報として各ノードにそれぞれ赤、黒の色を持っている。
また、通常の二分探索木の条件に加えて、各ノードが赤か黒の色を持つ、ルートノードの色は黒、葉ノードの色は黒、赤ノードは二つの黒ノードを子として持つ、ルートから末端のノードへの経路に含まれる黒ノードの数は一定などの条件を持つ。
%%RedBlackTree は通常の二分探索木の性質とは別に次のような性質を持っている。

%% \begin{itemize}
%%     \item 各ノードは赤か黒の色を持つ。
%%     \item ルートノードの色は黒である。
%%     \item 葉ノードの色は黒である。
%%     \item 赤ノードは2つの黒ノードを子として持つ(= 赤ノードが続くことは無い)。
%%     \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
%% \end{itemize}

数値を要素に持つ RedBlackTree の例を以下の図\ref{fig:rbtree}に示す。
条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。
加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。
%% atton-master fig3.1

%%%%figure
\begin{figure}[htpb]
   \begin{center}
       \includegraphics[width=50mm]{../pic/rbtree.pdf}
   \end{center}
   \caption{RedBlackTreeの例}
   \label{fig:rbtree}
\end{figure}

本研究で検証する RedBlackTree は非破壊であり、一度構築した木構造は破壊される操作ごとに新しい木が生成される。非破壊である理由は並列実行時のデータ保存である。


%% atton-master@13p

%% figure
%\begin{figure}[htbp]
%    \begin{center}
%        \includegraphics[width=50mm]{../pic/treeVnc.pdf}
%    \end{center}
%    \caption{構成される木構造}
%    \label{fig:tree}
%\end{figure}

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

\section{今後の課題}
現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。
今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。

\nocite{*}
\bibliographystyle{junsrt}
\bibliography{reference}
\end{document}