# HG changeset patch # User Yasutaka Higa # Date 1467368434 -32400 # Node ID bac0852b7258fc6b0e834d00598e78a519d540ed # Parent aeb1ce0e33c8a1586e97dc6f1099f231fa243bec Wrote section 2 diff -r aeb1ce0e33c8 -r bac0852b7258 paper/vmpcbc.tex --- a/paper/vmpcbc.tex Fri Jul 01 19:05:53 2016 +0900 +++ b/paper/vmpcbc.tex Fri Jul 01 19:20:34 2016 +0900 @@ -92,6 +92,25 @@ プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタコードセグメントを切り替えるだけでプログラムの信頼性を上げることができる。 \section{Continuation based C} +コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C 言語が存在する。 % TODO ref +Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 % TODO 要出典 +CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。 +コードセグメントどうしの接続は goto によって表される。 + +% TODO: かんたんな goto program + +また、データセグメントは構造体と共用体を用いたデータ構造を用いる。 + +CbC におけるメタコードセグメントは goto する際に必ず通るコードセグメント(以下の例では \verb/meta/ がそれにあたる)として表現される。 + +% TODO: meta を使った program +メタコードセグメントの切り替えは \verb/meta/ の切り替えで表現できる。 +メタデータセグメントはデータセグメントをフィールドに持つ構造体として表現できる。 + +CbC におけるメタ計算の例にメモリの管理がある。 +メモリの確保やポインタの演算をメタコードセグメントで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。 +また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。 + \section{メタ計算を用いたデータ構造の性質の検証} \section{まとめと今後の課題}