--- a/paper/chapter/introduction.tex	Sun Jan 31 11:36:32 2021 +0900
+++ b/paper/chapter/introduction.tex	Sun Jan 31 11:43:21 2021 +0900
@@ -16,15 +16,16 @@
 
 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
 形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。
-証明を用いる方法ではAgda\cite{agda}やCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
+証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
 Curry-Howard同型対応則により、型と論理式の命題が対応する。
 この型を導出するプログラムと実際の証明が対応する。
-特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
-証明そのものは記述した関数の内容の整合性を、定理証明支援系が検証する。
+証明には特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
+整合性の確認は、記述した関数を元に定理証明支援系が検証する。
 証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
 AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。
 しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
 Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。
+検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。
 検証ができているソースコードそのものを使ってOSを動作させたい。
 
 
@@ -42,7 +43,8 @@
 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
-この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。\cite{hyperkernel}
+この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel}
+証明しやすい表現の例として、 状態遷移ベースでの実装がある。
 
 
 証明を行う対象の計算は、 その意味が大きく別けられる。

Binary file paper/master_paper.pdf has changed

--- a/paper/reference.bib	Sun Jan 31 11:36:32 2021 +0900
+++ b/paper/reference.bib	Sun Jan 31 11:43:21 2021 +0900
@@ -146,6 +146,11 @@
 year      = {2004}
 }
 
+@manual{coq,
+  author = "{the coq proof assistant}",
+  title ="{\url{https://coq.inria.fr/}}",
+}
+
 @manual{gcc,
 author = "{GNU Compiler Collection (GCC) Internals}",
 title ="{\url{http://gcc.gnu.org/onlinedocs/gccint/}}",