# HG changeset patch # User Yasutaka Higa # Date 1467365496 -32400 # Node ID a9e93aee0af1554d235c73ecc49020174014ba3a # Parent 84ee0b8dc02e36962adea4f480e6ff2540ed19f7 Fix Newline code diff -r 84ee0b8dc02e -r a9e93aee0af1 paper/vmpcbc.tex --- 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}