# HG changeset patch # User Yasutaka Higa # Date 1467611421 -32400 # Node ID 84f71cc1764a29b6fa0cc7eda4e09b4cd4740661 # Parent 92136f6749899743abc630b93f798fb1bb76528d Add bibliographies diff -r 92136f674989 -r 84f71cc1764a paper/vmpcbc.tex --- a/paper/vmpcbc.tex Mon Jul 04 14:22:10 2016 +0900 +++ b/paper/vmpcbc.tex Mon Jul 04 14:50:21 2016 +0900 @@ -94,8 +94,8 @@ プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタコードセグメントを切り替えるだけでプログラムの信頼性を上げることができる。 \section{Continuation based C} -コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C 言語が存在する。 % TODO ref -Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 % TODO 要出典 +コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cbc-clang} 言語が存在する。 +Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。 コードセグメントどうしの接続は goto によって表される。 @@ -115,7 +115,7 @@ \section{メタ計算を用いたデータ構造の性質の検証} CbC で記述されさデータ構造と、データ構造に対する処理の性質を実際に検証する。 -検証の対象として、当研究室で CbC を用いて開発している Gears OS における非破壊赤黒木を用いる。 +検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{gears-os}における非破壊赤黒木を用いる。 赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。 @@ -131,7 +131,7 @@ 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc を用いてこの仕様を検証した。 akasha では検証用の仕様をメタコードセグメントに定義する。 検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。 -akasha を用いて要素数12個までは任意の順で挿入を行なっても仕様が満たされることを検証した。 % todo: だっけか +akasha を用いて要素数13個までは任意の順で挿入を行なっても仕様が満たされることを検証した。 また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。 CbCは C とほぼ同じ構文を持つため、単純な置換でC言語に変換することができる。 @@ -153,43 +153,9 @@ さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。 \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}. +\bibitem{cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014) +\bibitem{gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016) \end{thebibliography}