\documentclass[submit,PRO]{ipsj}
\usepackage{PROpresentation}
\PROheadtitle{y-n-(x): 情報処理学会プログラミング研究会 発表資料 Y年m月d日}

\usepackage{graphicx}
\usepackage{latexsym}

\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}

\setcounter{巻数}{57}
\setcounter{号数}{1}
\setcounter{page}{1}


\受付{2015}{3}{4}
%\再受付{2015}{7}{16}   %省略可能
%\再再受付{2015}{7}{20} %省略可能
\採録{2015}{8}{1}




\begin{document}


\title{Continuation based C を用いたプログラムの検証手法}
\etitle{Verification method of programs using Continuation based C}

\affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\
Infomation Engineering Course Graduate School of Engineering and Science University of the Ryukyus}
\affiliate{RUniv}{琉球大学\\
University of the Ryukyus}


\author{比嘉 健太}{Yasutaka HIGA}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。
Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。
Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。
プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。
また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。
Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。
本論文では Continuatoin based C によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。
\end{abstract}


\begin{jkeyword}
プログラミング言語, 検証, 赤黒木
\end{jkeyword}

\begin{eabstract}
We propose a verification method for programs using Continuation based C language.
Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment.
Code segments are calculation units which have input/output data segments that data unit.
Programs are represented by connections among with code segments and code segments.
The output data segment of some code segment is converted to the input data segment of connected one.
We introduce meta computations which split main computations and complicated computations such as memory control, error handling and more.
Meta computations represented to meta code segment and meta data segment, which saves main computations.
In this paper, We define a meta computation which connects code segments with verifications and verify properties of data structures such as Red-Black Tree and Synchronized Queue.
\end{eabstract}

\begin{ekeyword}
Programming Language, Verification, Red-Black Tree
\end{ekeyword}

\maketitle

\section{コードセグメントとデータセグメント}
\section{Continuation based C}
\section{メタ計算を用いたデータ構造の性質の検証}
\section{まとめと今後の課題}

\begin{thebibliography}{9}
\bibitem{okumura}
奥村晴彦：改訂第5版 \LaTeXe 美文書作成入門，
技術評論社(2010).

\bibitem{companion}
Goossens, M., Mittelbach, F. and Samarin, A.: {\it The LaTeX Companion},
Addison Wesley, Reading, Massachusetts (1993).

\bibitem{book1}
木下是雄：
理科系の作文技術，
中公新書(1981).

\bibitem{book2}
Strunk, W.J. and White, E.B.: {\it The Elements of Style, Forth Edition},
Longman (2000).

\bibitem{book3}
Blake, G. and Bly, R.W.: {\it The Elements of Technical Writing},
Longman (1993).

\bibitem{book4}
Higham, N.J.:
{\it Handbook of Writing for the Mathematical Sciences},
SIAM (1998).

\bibitem{webpage1}
情報処理学会論文誌ジャーナル編集委員会：
投稿者マニュアル(オンライン)，
\urlj{http://www.ipsj.or.jp/journal/ submit/manual/j\_manual.html}%
\refdatej{2007-04-05}.

\bibitem{webpage2}
情報処理学会論文誌ジャーナル編集委員会：
べからず集(オンライン)，
\urlj{http://www.ipsj.or.jp/journal/\\ manual/bekarazu.html}%
\refdatej{2011-09-15}.

\end{thebibliography}

\begin{biography}
\profile{m,E}{情報 太郎}{1970年生．1992年情報処理大学理学部情報科学科卒業．
1994年同大学大学院修士課程修了．同年情報処理学会入社．オンライン出版の研究
に従事．電子情報通信学会，IEEE，ACM 各会員．}
%
\profile{n}{処理 花子}{1960年生．1982年情報処理大学理学部情報科学科卒業．
1984年同大学大学院修士課程修了．1987年同博士課程修了．理学博士．1987年情報処
理大学助手．1992年架空大学助教授．1997年同大教授．オンライン出版の研究
に従事．2010年情報処理記念賞受賞．電子情報通信学会，IEEE，IEEE-CS，ACM
各会員．}
%
\profile{h,L}{学会 次郎}{1950年生．1974年架空大学大学院修士課程修了．
1987年同博士課程修了．工学博士．1977年架空大学助手．1992年情報処理大学助
教授．1987年同大教授．2000年から情報処理学会顧問．オンライン出版の研究
に従事．2010年情報処理記念賞受賞．情報処理学会理事．電子情報通信学会，
IEEE，IEEE-CS，ACM 各会員．}
\end{biography}



\end{document}