\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{Agda と継続を用いたプログラムの検証 \\ Verification of program using Agda and continuation}
\author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
\date{}
\twocolumn [
\maketitle
\begin{onecolabstract}
  % 高い信頼性を持つことは重要である。  
  % 私たちはプログラムの信頼性を高めるためにCodeGear、DataGearという単位でプログラ
  % ムを書くことを提案している。
  % そのためにCodeGear、DataGearという単位を使える言語 CbC を開発している。
  % CbC では既存の実装でのデータの取扱が複雑になっている。
  % そのためにDataGearとCodeGearを Interface という単位でまとめた。
  % これら単位をAgdaでも使えるようにし、CbC で記述した Stackや Tree を Agda に
  % 変換した。
  % この論文ではそれらに対して幾つかの部分的な証明を試みた。

  Program has high reliability. it is important.
  we are proposing to write program in units of CodeGear, DataGear for increase
  the reliability.
  we are deceloping Continuation based C (CbC) that can use units CodeGear and
  DataGear.
  In CbC, the handling of data in existing implementations is complicated.
  for that purpose, we can provide a interface mechanisms which are packages of
  CodeGears and DataGears.
  we made these units and interface available for Agda.
  Also converted Stack and Tree wrote in CbC to Agda.
  In this papaer, we tried several proofs on them.
% 
% (we are mapping this units to Agda)
% CbC では CodeGear 、 DataGear という単位でプログラミングできる。
% ~~
% Agda で interface を実装
% interface を含めて証明ができるか
% codeとcode のあいだをcall ではなくjmpで結ぶことができる(goto)
%gotoをつかうことによりOSに必須なmeta計算を実現できる
%メタ計算は例えばメモリ管理スレッド管理CPUやGPUの資源管理そしてData/Code Gear の管理などである
%metaレベルではcode/data gear は一つの塊として操作される。これをcbcではunion dataとして実装している
%code gear 間の接続はつぎのcode gearの番号とthread structure に相当するcontextをmeta code gear にgoto する
%meta code gear で os の 機能であるメモリ管理やスレッド管理を行う。
%ユーザーレベルではmeta構造を直接見ることはなく、継続を用いた関数型プログラミングに見える
%metaレベルから見たdata gearをゆーざーれべるのcode gearに接続するにはstub というmeta code gear  を用いる
%stubとmetaはユーザーレベルcodegear とdatagearから生成することができる
%本論文ではstub とcontext 管理構造を生成するスクリプトを作成した
%これによりcode gear とdeta gear をデータを操作するinterface というまとまりにすることができる。
% CbC gives Code Gear and Data Gear as programing units.
% A transfer from a Code Gear to another Code Gear is implemented using a CbC's goto statement,
% which is compiled as a jump instruction in CbC. 
% CbC's goto statements provides a ways of implementing meta computations.
% From a view point of meta computation, Data Gear or Code Gear are uniform data units, which are implemented
% as union Data in CbC. 
% In the meta level, a transfer from a Code Gear is a goto statement to meta Code Gear with next Code Gear number and 
% a Context which corresponds thread structure or an environments in a functional programing.
% From a normal level, meta structures are not visible directly and a Code Gear looks like a function using continuations.
% A stub Code Gear is used as a bridge between meta level and normal level.
% we can generate meta Code Gear and stub Code Gear from normal level Code Gear,
% and provide a interface mechanisms which are packages of Code Gears and Data Gears.
\end{onecolabstract}]
\thispagestyle{fancy}

% ソフトウェアの信頼性の保証
% 　　CbC の話(CG,DGの話も)
% 　　メタ計算を分けてる
%    context (Meta DataGear)
%    そのために interface
%    Agda でも interfece を実装して検証した

\section{ソフトウェアの信頼性の保証}
ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証す
る方法として代表的なものはモデル検査と、定理証明が存在している。
当研究室では検証しやすいプログラムの単位として、 CodeGear と DataGear という単位
を用いるプログラミングスタイルを提案している。
また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語として
Countinuation based C (以下 CbC) を開発している。
% 本研究では、検証や証明に直接使用できる言語として CbC を用いる。

CbC では通常の計算とメタ計算を分けて記述している。
しかし、CodeGear で DataGear を扱う際、 Context と呼ばれる CodeGear、 DataGear の
リスト等を持っている Meta DataGear を経由する。
通常の CodeGear から Meta DataGear である Context を直接扱えると、ユーザーがメタ
計算をノーマルレベルで自由に記述できてしまい、信頼性を損なう。そのため、 CbC
では Context を通して、次の CodeGear に接続する Meta CodeGear である stub
 CodeGear を定義している。

CbC で実装していくにつれて特殊な stub CodeGear の記述が複雑になった。
そこで既存の実装をモジュールとして扱うために Interface という仕組みを導入した。
Interface では、DataGear に対しての操作(API)を CodeGear とその CodeGear で扱われ
ている DataGearの集合を抽象的に表現した Meta DataGear として定義されている。

本研究では CbCで使われている Interface を 、 Agda 上で定義、実装を行い、
Interface を含めた Stack と Tree の部分的な証明を行なった。

\section{Countinuation based C (CbC)}
Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。
CbC は C 言語とほぼおなじ構文を持つが、 C の関数の代わりに CodeGear を用いて処理
を記述する。
CodeGear は関数定義の先頭に $\_\_code$ をつけて定義する。
CodeGear は処理の単位でそれらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。
DataGear は CodeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。次の CodeGear に処理を移す際は、 goto の後に CodeGear 名と DataGear を指定する。
CbC ではこの継続処理がメタ計算として定義されており、通常計算である CodeGear を変
更することなく検証や資源管理等の記述を行うことができる。
例として CbC の簡単な例(ソースコード\ref{src:goto})と、流れ\ref{fig:code_simple}を示す。

\lstinputlisting[label=src:goto, caption=CbCコードの例]{./src/goto.cbc}
\begin{figure}[htpb]
 \begin{center}
   \scalebox{0.7}[0.7]{\includegraphics{fig/codesegment.pdf}}
 \end{center}
 \caption{ソースコード\ref{src:goto}の流れ}
 \label{fig:code_simple}
\end{figure}

ソースコード\ref{src:goto}では　cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、
cs1 の Input DataGear になる。
流れ\ref{fig:code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継
続に指定された CodeGear へ継続する。

\section{CbC における Interface の定義}
CbC で実装していくにつれ、stub CodeGear の記述が煩雑になった。
そのため 既存の実装を モジュールとして扱うため Interface を導入した。
Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear
として定義した。例として Stack での Interface の実装(ソースコード\ref{src:interface})を示す。

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

元の実装の push では Stack を指定する必要があるが、
Interface での実装は push 先の Stack が stackImpl として扱
われている。この stackImpl は呼ばれた時の Stack と同じになる。
これにより、 ユーザーは実行時に Stack を指定する必要がなくなる。
このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
しが容易になる。

\section{Agda}
Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。
依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。
CbC を Agda に変換する場合 DataGear はレコード型、 CodeGear は Agda での通常関数
として定義できる。
前項で示した CbC の簡単な例を Agda に変換する。(ソースコード\ref{src:agda-css})

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

Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。
関数の型では → または \verb/->/ を使い定義し、関数本体は関数名の後に$=$をつけて
記述する。
DataGear はレコード型で表記できるため Agda 上で DataGear を定義することが可能で
ある。
 % 定義をする際は record キーワードのあとにレコード名、
% 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー
% ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙
% していく。複数の値を列挙する際は ; で区切る。
% Agda での DataGear の定義の例を以下のソースコード\ref{src:agda-ds}示す
% \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
このように CbC のコードを Agda に変換し、証明を行う。

\section{Agda における Interface の定義、実装}
Agda でも CbC と同様に Interface の定義、実装した。
例として Agda で実装した Stack-interface の一部をみる。
Stack の定義はソースコード\ref{src:agda-interface}、実装は ソースコード
\ref{src:agda-single-linked-stack}
として書かれている。それを Stack 側から interface を通して呼び出している。

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

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

\section{Agda による Interface 部分を含めた Stack の部分的な証明}
今回は Interface を通した Stack で push
、 pop などの操作が正しく行われるかの証明を行った。
ここでの証明とは Stack が特定の性質を持つことを保証することである。

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

まず始めに不定状態の Stack をソースコード~\ref{src:agda-in-some-state}
で定義した。 stackInSomeState が不定状態の Stack である。
 ソースコード~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対し
 て、 push を2回行い、 pop2 をして取れたデータは push したデータと同じものになる
 ことの証明している。

 \lstinputlisting[label=src: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$で両方共に成り立つ為、
 refl で推論が通る。
これにより、抽象化した Stack に対して push を2回行い、 pop を行うと push したものと同じも
のを受け取れることが証明できた。
 
\section{まとめ}
本研究では CodeGear、 DataGear を用いたプログラミング手法を用いて、Agda で
Interface を用いたプログラムを実装、検証した。
また、 CbC で記述した時には細かく分かっていなかった Interface の型が明確に
なった。
今後の課題としては、Tree 側では証明が複雑化し、うまく証明できていないことと、
 Hoare Logic 用いての証明を行えるように、CodeGear、DataGear をベースにした Hoare
 Logic を Agda 上で定義し、実際に証明を行うことなどが挙げられる。

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