\documentclass[a4j,9.5pt]{jarticle}
% \usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage[]{multicol}
\usepackage{listings,jlisting}
%\pagestyle{fancy}
\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}


\usepackage{ascmac}
\usepackage[dvipdfmx]{graphicx}
\usepackage{amssymb}
\usepackage{type1cm}
\usepackage[usenames]{color}
\usepackage{ulem}

\renewcommand{\abstractname}{要 旨}
\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\small\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.3pt,
  columns=[l]{fullflexible},
  numbers=none,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=2em,
  language={},
  tabsize=4,
  lineskip=-0.1zw,
  escapechar={@},
}

\begin{document}
\title{Continuation based C での Hoare Logic を用いた赤黒木の検証 \\ Validation of red-black tree implemented in Continuation based C using Hoare Logic}
\author{学籍番号 175706H 氏名 上地 悠斗 \\ 指導教員 : 河野 真治}
\date{}
\maketitle
\thispagestyle{fancy}

% 要旨
\input{./tex/abstract/abstract.tex}

\begin{multicols}{2}
\input{./tex/intro/intro.tex}

\section{Continuation based C}
	前述した通り CbC とはC言語からループ制御構造とサブルーチンコールを取り除き、
	継続を導入したC言語の下位言語である。継続呼び出しは引数付き goto 文で表現される。
	また、CodeGear を処理の単位、DataGear をデータの単位として記述するプログラミング言語である。
	CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。

\subsection{Code Gear / Data Gear}
	CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いるプログラミングスタイルを提案している。

	CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。
	DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
	CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。
	
	CodeGear 間の移動は継続を用いて行われる。
	継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、次の CodeGear へ継続を行う。
	これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。


\subsection{Meta Code Gear / Meta Data Gear}
	プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
	資源管理等を記述しなければならない処理が存在する。
	これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。

	メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
	そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。

	Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
	CodeGear を実行する前後やDataGear の大枠として Meta Gear が存在している。

	例として CodeGear が DataGear から値を取得する際に使われる、 stub CodeGear について説明する。

	CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが
	必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。
	これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。
	そのために、 Meta CodeGear として Context から必要な DataGear を取り出し、
	CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。

	Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub
	CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear
	のメモリ空間等を持った Meta DataGear を扱っている。


\section{Hoare Logic}
	Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
	これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
	というもので、CbCの実行を継続するという性質に非常に相性が良い。
	Hoare Logic を表記すると以下のようになる。
	$$ \{P\}\ C\ \{Q\} $$
	この3つ組は Hoare Triple と呼ばれる。

	Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。

	Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
	これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。

\section{agda}
	agdaとは、Agda は依存型をもつ純粋関数型の言語である。 定理証明支援器でもある。

\section{関連研究}
	外間による研究では CbC にて実装された While Loop を Hoare Logic を用いて検証した。

\section{検証手法}
    手法は模索中であり、先行研究と同じ手法を取ろうとしている。本章では先行研究で述べられている検証手法について説明する。

% 手法
\input{./tex/spec/spec.tex}

\section{今後の課題}
    d

\section{類似技術}

\subsection{coq}

\begin{thebibliography}{9}

\bibitem{1}CbCの論文
\bibitem{2}外間先輩の先行研究
\bibitem{3}Hoare Logicの論文
\bibitem{4}Hoare Logicのスライド
\bibitem{5}agda のサイト
\bibitem{6}Aaron Stumpの本
\bibitem{7}atttonさんの論文
\bibitem{8}Haskell
\bibitem{9}Coq

\end{thebibliography}
\end{multicols}

\end{document}