--- a/paper/vmpcbc.tex	Tue Jun 28 18:27:26 2016 +0900
+++ b/paper/vmpcbc.tex	Fri Jul 01 18:31:36 2016 +0900
@@ -1,138 +1,138 @@
-\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}
+\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}