# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1588225157 -32400
# Node ID 1e8d8d32fe3072815a19a950a93b059c09edc1ec
# Parent  d43b107ad19951b1af4fca39e710940e721009ab
...

diff -r d43b107ad199 -r 1e8d8d32fe30 paper/anatofuz-sigos.md
--- a/paper/anatofuz-sigos.md	Thu Apr 30 14:23:51 2020 +0900
+++ b/paper/anatofuz-sigos.md	Thu Apr 30 14:39:17 2020 +0900
@@ -17,6 +17,12 @@
 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
 
 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
-現在小さなunixであるxv6 kernelを状態遷移を基本とした単位でのプログラミングに適した言語、 Continuation Based Cを用いて再実装している。
-再実装の為には、 既存のxv6 kernelの処理の状態遷移を、継続を用いたプログラムに変換していく必要がある。
+CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
+Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
+すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードをプログラミングできる。
 
+現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
+再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
+本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
+
+