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



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

CbC では自由に DataGear を扱う際に直接 CodeGear からアクセスできてしまうと信頼性を損ねる。
その為に stub CodeGear と呼ばれるデータを扱うための Meta CodeGear を定
義している。基本的な stub CodeGear は CodeGear から自動で生成することができるよ
うになっている。
しかし、 CbC で実装していくにつれて stub CodeGear の記述が複雑になることが分かっ
た。　その為、既存の実装をモジュールとして扱うために Interface という仕組みを導
入した。

本研究では CbC 、 Agda の両方で Interface を実装し、 Interface を含めた Stack と Tree の性質を
部分的に証明した。

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

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

push では新しい element を作成し next に現在の top を入れ、Stack の top を書き換えて次のCodeGearに飛ぶ。
pop では top に data があればそれを next に入れ、 Stack を更新して次のCodeGearに飛ぶ。 top に data が無ければ NULL を next に入れて次のCodeGearに飛ぶ。

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

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

% Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。関数の型では → または \verb/->/ を使い定義する。
% Agda のレコード型も存在する。定義をする際は record キーワードのあとにレコード名、
% 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー
% ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙
% していく。複数の値を列挙する際は ; で区切る。DataGear はレコード型で表記できた
% ため、 Agda での DataGear の変換はレコード型を使う。 
% このように CbC のコードを Agda に変換し、証明を行う。

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

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

\section{Agda による Interface 部分を含めた Stack の部分的な証明}
Agda で Interface を定義する事ができた。この 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 の型が明確に
なった。
今後の課題としては、CodeGear、DataGear をベースにした Hoare Logic を Agda で実装する。
また、その Hoare Logic を使い、いくつかの証明を実際に記述する。

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