Binary file Paper/master_paper.pdf has changed

--- a/Paper/master_paper.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/master_paper.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -132,13 +132,13 @@
 実際に Invariant を用いることで,プログラムに与える入力とその出力に対して条件を与え,Hoare Logic による検証を行えるようになった.
 これにより,いままでより容易に Gears Agda にて検証が進められるようになった.
 
-また,先行研究での課題にて,CbCで開発,検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列並列動作の検証があった.これもモデル検査により,Gears Agda 内で並列動作に対する検証も行えるようになった.
+また,先行研究での課題にて,CbCで開発,検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列動作の検証があった.これもモデル検査により,Gears Agda 内で並列動作に対する検証も行えるようになった.
 
 
 \section{今後の課題}
 今後の課題としてモデル検査による検証,定理証明による検証,Gears Agda の今後の展望について述べる.
 モデル検査においては,有向グラフからなる有限オートマトンの遷移を全自動探索することと,live lockやLTTLも用いたアサーションなどの検証\cite{model}を行いたい.
-加えて,State List のデータ構造を brunced tree にすることで,並列にモデル検査が行えるようになると考えられる.
+加えて,State List のデータ構造を balanced tree にすることで,並列にモデル検査が行えるようになると考えられる.
 これにより,状態が膨大になるモデル検査に対応できる.
 
 定理証明においては,Red Black Tree の検証を行いたいと思っている.

--- a/Paper/tex/abst.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/abst.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,29 +1,30 @@
 \chapter*{要旨}
+
 開発手法の一つとして，形式手法というものがある．
 形式手法とはプログラムの仕様を形式化，つまり数学的な記述を行い，
-書いたプログラムがそれを満たしているか検証を行う手法である．
+書いたプログラムがそれを満たしているか検証を行う開発手法である．
 代表的な形式の検証手法として，定理証明やモデル検査が挙げられる．
 
-形式手法で開発したプログラムは数学的に正しいことが証明されている，
+形式手法で開発したプログラムは数学的に正しいことが証明されている.
 そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている．
-しかし,一見完璧な手法であるように思えるが欠点として，膨大なコストを要する．
-シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用せずとも良いとなる．
+一見完璧な手法であるように思えるが欠点として，形式化や検証が複雑なため膨大なコストを要する．
+シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用する利点が薄くなる．
 
-そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
-Gears Agdaとは当研究室で開発している Continuation based C (CbC) の概念を
-取り入れた記法で記述された Agdaのことである．
+そのため，他のプログラミング言語と比べて検証に適している Gears Agda を使用する．
+Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を
+取り入れた記法で記述された定理証明支援器 Agda のことである．
 
 定理証明によるプログラムの検証は一般的に難易度が高いが，
 Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている．
 
 先行研究では implies を用いて Hoare Logic での定理証明を行っていた.
-しかしそれでは記述が長く,かつ複雑になってしまっていた.
-そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行を行うことで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった.
+しかし、それでは記述が長く複雑になっていた.
+そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行をすることで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった.
 
-また，定理証明では並行処理の検証は困難である.
+また，定理証明では並列処理の検証は困難である。出現する状態を一度全て出してからそれらの検証を行わないといけないためである。
 そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした．
 
-これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる
+これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる。
 
 \chapter*{Abstract}
 One of the development methods is called formal methods.

--- a/Paper/tex/agda.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/agda.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -2,8 +2,8 @@
 Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である．
 Agda は依存型という型システムを持ち，型を第一級オブジェクトとして扱う．
 
-また,もともとの Agda には自然数などの定義すら存在しない.
-その実装ができることも本章で取り扱っているが,一般的には standard-libralies \cite{agda-stdlib} を使用する.
+また,もともとの Agda には自然数などの普遍的な定義すら存在しない.
+その実装ができることも本章で取り扱っているが,一般的には agda-standard-libralies \cite{agda-stdlib} を使用する.
 
 本章ではAgdaの基本とAgdaによる定理証明の方法について述べる.
 
@@ -21,27 +21,27 @@
 \verb/data/ キーワードの後に \verb/data/ の名前と，型， \verb/where/ 句を書きインデントを深くし，
 値にコンストラクタとその型を列挙する．
 
-Code \ref{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である．
+\coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)の例である．
 
-\lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}
+\lstinputlisting[label=code:agda-nat, caption=自然数を表すデータ型 $\mathbb{N}$ の定義] {src/nat.agda.replaced}
 
 \verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である．
-\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており，
+\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を返す再帰的なデータになっており，
 \verb/suc/ を連ねることで自然数全体を表現することができる．
 
 $\mathbb{N}$ 自身の型は \verb/Set/ であり，これは Agda が組み込みで持つ「型集合の型」である．
 \verb/Set/ は階層構造を持ち，型集合の集合の型を指定するには \verb/Set1/ と書く．
 %% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる．
 
-Agda には C 言語における構造体に相当するレコード型というデータも存在する，
-例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する．Code \ref{agda-record}のようになる．
-\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced}
+Agda には C 言語における構造体に相当するレコード型というデータも存在する。
+例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する．\coderef{agda-record}のようになる．
+\lstinputlisting[label=code:agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced}
 レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する．
 複数の値を列挙するには \verb/;/ で区切る必要がある．
 
 %% 関数について
 Agda での関数は型の定義と，関数の定義をする必要がある．
-関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが，入力を受け取り出力返す型として記述される．$\rightarrow$ ， または\verb/→/ を用いて \verb/input → output/ のように記述される．
+関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが，入力を受け取り出力を返す型として記述される．または $\rightarrow$ を用いて \verb/input → output/ のように記述される．
 また，\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し，中間記法で関数を定義することもできる．
 関数の定義は型の定義より下の行に，\verb/=/ を使い \verb/name input = output/ のように記述される．
 
@@ -120,7 +120,7 @@
 ここでは，\verb/+zero/ を利用し， \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり，左右の項が等しいことを示す \verb/refl/ になっている．
 
 \lstinputlisting[caption=congを用いた等式変形の例,label=code:agda-term-post]{src/agda-term3.agda.replaced}
-\coderef{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし，\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した．
+\coderef{agda-term-post} では \verb/suc (y + x)/ $\equiv$ \verb/y + (suc x)/ という等式に対して $\equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $\equiv$ \verb/suc (y + x)/の形にし，\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した．
 これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた．
 
 Agda ではこのような形で等式を変形しながら証明を行う事ができる．

--- a/Paper/tex/cbc.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/cbc.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,7 +1,7 @@
 \chapter{Continuation based C}
-Continuation based C\cite{kaito-lola} （以下 CbC） は 
+Continuation based C\cite{kaito-lola}は 
 関数呼び出しの際にjmp命令で遷移をし，環境を持たずに遷移する
-ことができるC言語である，
+ことができるC言語である。
 すなわちC言語の下位言語にあたり，よりアセンブラに近い記述を行う．
 
 CbC では CodeGear を処理の単位，
@@ -9,7 +9,6 @@
 
 jmp命令で関数遷移するため関数遷移し実行が終了しても，もとの関数に戻ることはない．
 そのため次に遷移する Code Gear を指定する．
-これは，関数型プログラミングでの末尾関数呼び出しに相当する．
 したがって，Code Gear に Deta Gear を与え，それをもとに処理を行い，
 出力として Data Gear を返し，また次の Code Gearに遷移していく流れとなる．
 
@@ -23,7 +22,7 @@
 CodeGear の入力となる DataGear を Input DataGear と呼び,出力は Output DataGear と呼ぶ.
 
 CodeGear 間の移動は継続を用いて行われる.
-継続は関数呼び出しとは異なり,呼び出した後に元のコードに戻れず,次の CodeGear へ継続を行う.
+継続は関数呼び出しとは異なり,呼び出した後に元のコードに戻れず,次の CodeGear へ遷移を行う.
 これは,関数型プログラミングでは末尾再帰をしていることと同義である.
 
 
@@ -31,7 +30,7 @@
 同じ仕様でCbCとC言語で実装した際の違いを,実際のコードを元に比較する.
 比較するにあたり,再起処理が含まれるコードの例として,
 フィボナッチ数列の n 番目を求めるコードを挙げる.
-C言語で記述したものが\coderef{fib_c}.CbCで記述したものが\coderef{fib_cbc}になる.
+C言語で記述したものが\coderef{fib_c}になり、CbCで記述したものが\coderef{fib_cbc}になる.
 CbCは実行を継続するため, return を行えない.そのためC言語での実装も return を書
 かず関数呼び出しを行い,最後にexitをして実行終了するように記述している.
 
@@ -42,8 +41,8 @@
 
 軽量実装になっているのか,上記のコードをアセンブラ変換した結果を見て確認する.
 全てを記載すると長くなるので,アセンブラ変換した際のfib関数のみを記載する.
-C言語で記述した\coderef{fib_c}をアセンブラ変換した結果が\coderef{c-ass}.
-CbCで記述した\coderef{fib_cbc}をアセンブラ変換した結果が\coderef{cbc-ass}になる.
+C言語で記述したコードをアセンブラ変換した結果が\coderef{c-ass}.
+CbCで記述したコードをアセンブラ変換した結果が\coderef{cbc-ass}になる.
 
 比較すると,fib 関数の内部で再度 fib 関数を呼び出す際,
 C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している.

--- a/Paper/tex/cbc_agda.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/cbc_agda.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,6 +1,6 @@
 \chapter{GearsAgda 形式で書く Agda}
 CbC の継続の概念を取り入れた Agda の記法を説明する．
-Agdaでは関数の再帰呼び出しが可能であるが，CbCでは値が 帰って来ない．そのためAgda
+Agdaでは関数の再帰呼び出しが可能であるが，CbCでは値が帰って来ない．そのためAgda
 で実装を行う際には再帰呼び出しを行わないようにする．
 
 以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する．
@@ -22,50 +22,52 @@
 最初に関数名のあとに:（コロン）の後ろに命題を記述し，
 そのあとに関数名のあとに引数を書き，=（イコール）の後ろに定義を記述している．
 
-\lstinputlisting[caption= Agdaでの 停止性が示せない CodeGear の例, label=agda-not-cg, firstline=18, lastline=22]{src/agda/cbc-agda.agda.replaced}
-
-\lstinputlisting[caption= Agdaでの CodeGear の初期化, label=agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced}
-
 Gears Agda での Code Gear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で終了するようになっている．
 この （Env $\rightarrow$ t） は引数で受け取る型で Env を受け取ってtを返すという意味になる．
 これが Code Gear を実行したあとの末尾関数呼び出しを行う次の Code Gear となる．
 最後にtを返すのは，これ自体が Code Gear であることを示している．
 
 引数を受け取ったあとに別の関数に再度渡している．
-これは後述するが，Agda の繰り返し処理を行う際に停止性を見失うために減少列を引数に取っている．
+これは，Agda の繰り返し処理を行う際に停止性を見失うために減少列を引数に取っている．
 内部の処理は reducer を減らしながらvarxを増やし，
 vary の値を varx に与えていくことで足し算を定義している．
 基本的に繰り返し実行するコードを実装する場合には，
 実行時に減少しその関数がいずれ停止することを示す reducer を含めるようにしている．
 
-reducerを含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す．
+対照的に reducer を含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す．
+
+\lstinputlisting[caption= Agdaでの 停止性が示せない CodeGear の例, label=agda-not-cg, firstline=18, lastline=22]{src/agda/cbc-agda.agda.replaced}
+
 Agdaではパターンマッチを行うことで場合分けを考えることができるが，
 受け取った Code Gear であるenvを with を使用してパターンマッチを試みている．
 パターンマッチ自体は可能だが，この方法だとAgdaが関数が停止することを認識できない．
-そのため，\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし
+そのため，\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし、
 この関数が停止することを記述してコンパイルが通るようにしている．
 
 Code \ref{agda-exec-cg} は受け取った引数で Data Gear を初期化して
 それを Code Gear に与えることで実行を行っている．
-今回の例では 引数から Data Gear を作成するのは
-複雑ではないため，一度で Data Gear を作成してそれを Code Gear に渡している
-引数から Data Gear を作成するのが複雑な場合は一度 入力から
+
+\lstinputlisting[caption= Agdaでの CodeGear の初期化, label=agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced}
+
+今回の例では 引数から Data Gear を作成するのは複雑ではない。
+そのため，一度で Data Gear を作成してそのまま Code Gear に渡している。
+引数から Data Gear を作成するのが複雑な場合は、一度入力から
 Data Gear を作成する Code Gear を用いる．
-加えて，実行なので命題の部分の最後が Env になっている．
+加えて，実行なので命題の部分にある出力の型は Env になっている．
 
 \section{Agda による Meta Gears}
 通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である．
-今回はモデル検査を行う際に使用する \cite{atton-master}
+今回は定理証明やモデル検査を行う際に使用する \cite{atton-master}。
 
 \begin{itemize}
 \item Meta DataGear \mbox{}\\
   Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる．
   通常の Data Gear を wraping している．
-  今回はこれを用いることで，定理証明では不変状態の条件を保存し，モデル検査ではその時点での状態を保存する
+  今回はこれを用いることで，定理証明では不変状態の条件を保存し，モデル検査ではその時点での状態を保存する。
 
 \item Meta CodeGear\mbox{}\\
   Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
   である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
-  す CodeGear である．今回はここで定理証明やモデル検査を行う
+  す CodeGear である．今回はここで定理証明やモデル検査を行う。
 \end{itemize}
 

--- a/Paper/tex/dpp_impl.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,17 +1,13 @@
 \section{Gears Agdaによるモデル検査の流れ}
 今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている.
 
-- Gears Agda にてモデル検査を実装を行う
-  - step実行を行う Code Gear や,場合によっては分岐を行うCode Gearが必要になる
-
-- プログラムが実行中に取りうる状態の網羅をする State List を作成する.
-
-- 上で実装したものを使用しつつ,meta データである プロセスが実行するための wait list を定義する Meta Data Gear や分岐の数を保存する Meta Data Gear を定義する.
-
-- 上記 Meta Code Gear で作成された meta data を元に,dead lockを判定する Meta Code Gear を記述する
-
-
-- 状態を網羅した State List にある State を一つずつ Meta Code Gear に実行させて,dead lockしている状態がないか確認する
+\begin{enumerate}
+  \item Gears Agda にて DPP の実装を行う
+  \item プログラムが実行中に取りうる状態の網羅をする State List を作成する
+  \item 上で実装したものを使用しつつ Meta Data Gear を構築する Meta Code Gearを記述する
+  \item 上記 Meta Code Gear で作成された meta data を元に,dead lockを判定する Meta Code Gear を記述する
+  \item 状態を網羅した State List にある State を一つずつ Meta Code Gear に実行させて,dead lockしている状態がないか確認する
+\end{enumerate}
 
 先行研究では網羅した状態データを State DB に格納していた.しかし今回の Gears Agda では State List にて代替とした.これは List で行った方が Agda での実装がしやすい点にある.本来は branced tree をデータ構造に持って State を作成するほう正しい.
 
@@ -74,17 +70,16 @@
 
 最後の哲学者は一番最初のフォークを参照する必要がある．
 フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので
-それを自分の pid に書き換え left-hand を true に書き換えてフォークを手に持つ
+それを自分の pid に書き換える。次に left-hand を true に書き換えて手に持つ
 フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は
 状態を変化させずに処理を続ける．
 このように左のフォークを取る記述をした．
 
 右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る．
-比較するべき table の List と哲学者のListは一致しているため，put\_lfork のように最後の哲学者が
+比較するべき table の List と哲学者のListは一致しているため，pickup\_lfork のように最後の哲学者が
 最初のフォークを参照することもない．
 
-似たような形で哲学者がフォークを置く putdown-l/rfork を実装した．
-
+似たような形で哲学者がフォークを置く putdown-lfork/rfork を実装した．
 思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．
 
 \section{Gears Agda によるDPPの検証}
@@ -94,30 +89,31 @@
 ここからは,モデル検査を行うため,Meta Data Gear の定義をし,
 それの操作を行う Meta Code Gear の実装を行っていく.
 
-以下\coderef{dpp-mdg}がMeta Code Gear の定義になる
+以下\coderef{dpp-mdg}がMeta Data Gear の定義になる。
 
 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
-\lstinputlisting[caption=Gears Agdaでの DPP モデル検査を行うための Meta Data Gear の定義, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
+\lstinputlisting[caption=Gears Agda で DPP のモデル検査を行うための Meta Data Gear, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
 
 この Meta Data Gear の説明をすると,
 metadataは状態の分岐数を持っておくnum-brunchがある.
-MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)
-meta に 前述したmetadataを持っており,
+MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)となる。
+meta には前述したmetadataを持っており,
 他には,deadlockしているかのフラグである deadlock ,
-最後の2つは後述する際に必要になる.
+最後の2つは後に必要になるフラグである。
 そのstate が step 実行済みなのかのフラグであるis-step,
 そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている.
 
-MetaEnv2 は1つのstate である MetaEnv の Listを meta で持てる.
+MetaEnv2 は1つのstate である MetaEnv の Listを metal で持てる.
 加えて今まで実行していた Data Gear  を DG で持てる.
 
-次に Meta Data Gear を作成する Meta Code Gear の説明をすると
-
-- その状態から分岐できる状態数をカウントする Meta Code Gear
+次に Meta Data Gear を作成する Meta Code Gear の説明をする。
 
-- Wait List を作成する Meta Code Gear
+\begin{enumerate}
+  \item その状態から分岐できる状態数をカウントする Meta Code Gear
+  \item Wait List を作成する Meta Code Gear
+\end{enumerate}
 
-以下の \coderef{dpp-mcg-branch} が分岐できる状態数をカウントする Meta Code Gear となる
+以下の \coderef{dpp-mcg-branch} が分岐できる状態数をカウントする Meta Code Gear となる。
 
 %ここにコードを載せる%
 \lstinputlisting[caption=状態の分岐数をカウントする Meta Data Gear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced}
@@ -127,7 +123,7 @@
 
 つまり,この Meta Code Gear の実装にあたって新しい実装はほとんど行っていない.
 
-Wait List の 作成も同じように,取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとし,Wait Listに入れている.
+Wait List の 作成も同じように取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている.
 
 %いちおうコード載せようかな？←棄却されました%
 
@@ -138,7 +134,7 @@
 
 そして「num-brunchの値が1であり,wait Listの数がプロセス数と一致する」ということは,「その状態から別の状態に遷移することができない」として,この状態をdead lockであると定義した.
 
-以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる
+以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる。
 
 複雑なことは何もしておらず,単純にstate毎のnum-brunchの値を見て,wait-listの数がプロセス数と一致していた場合に
 deadlockのフラグを立ち上げている.これが,Gears Agda におけるアサーションになっている.
@@ -153,7 +149,7 @@
 しかし,分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる.
 存在していた場合はそれを追加せず,存在しなかった場合にのみ State を追加する.
 
-Agdaには2つの record が等しい場合の分岐など存在しないため,
+Agdaには2つの record が等しいか確かめる関数などは存在せず,
 \coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する.
 こちらはそのまま掲載すると長いので,実際のコードに手を加えて省略している.実際のコードは付録にて参照できる.
 
@@ -165,11 +161,11 @@
 
 更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し,次のstateの一致を探索するように記述されている.
 
-実際にstateの一致を見ているのは22行目のeq-env関数で,一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている
+実際にstateの一致を見ているのは22行目のeq-env関数で,一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている。
 
 State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている.
 その値が一致している場合には別の値を見て,一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている.
-他の値である,lhandやrhandなども同じように記述している.
+他の値である,lhandやrhandなども eq-pid と同じように記述している.
 
 
 これらにて,まだ分岐を見ていない1つのStateの分岐を確かめる.
@@ -179,7 +175,7 @@
 State List に存在している全ての state の分岐を見たということは,
 出現するStateを全て網羅することができたと言える.
 
-あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる
+あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる。
 
 \section{Gears Agda による live lockの検証方法について}
 live lockとは,状態が変動しているが,その状態はループしており,実行が進んでいないことを指す.
@@ -193,14 +189,14 @@
 
 history がloopしていた際に,誰もeathingしていない場合を live lock していると定義する.
 
-今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める.それがloop中に存在いしているかを見れば live lock を検知できる.
+今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める.それがloop中に存在しているかを確認することで live lock を検知できる.
 
 
 \section{Gears Agda でのモデル検査の評価}
 
-SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方が制約が多いため難解に思える.しかし,Gears Agda ではプログラムの実装も含んでいる.
+SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方がコードも長く、制約が多いため難解に思える.しかし,Gears Agda ではプログラムの実装も含んでいる.
 
-さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため,比較的容易であると言える.
+さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため,他のプログラムに適応できることを考えると比較的容易であると言える.
 
 加えて,Gears Agda は CbC へコンパイルされ,高速に実行されることを踏まえると,いかに Gears Agda が検証に向いたプログラムであるか理解できる.
 

--- a/Paper/tex/hoare.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/hoare.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -8,7 +8,7 @@
 R.W Floyd が考案したプログラムの検証の手法である．
 これは，「プログラムの事前条件(P)が成立しているとき，
 コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
-というもので，CbCの実行を継続するという性質に非常に相性が良い．
+というものである。これはCbCの実行を継続するという性質に非常に相性が良い．
 Hoare Logic を表記すると以下のようになる．
 $$ \{P\}\ C \ \{Q\} $$
 この3つ組は Hoare Triple と呼ばれる．

--- a/Paper/tex/intro.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/intro.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,29 +1,27 @@
 \chapter{Gears Agda でのプログラムの検証}
 
-OSやアプリケーションの信頼性の向上は重要である
+OSやアプリケーションの信頼性の向上は重要である。
 信頼性を向上するための手段として,プログラムを検証する事が挙げられる.
 
-
-しかし,検証には仕様の形式化とその検証には膨大なコストを要する．
-そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
-Gears Agdaとは当研究室で開発している Continuation based C \cite{cbc-gcc}(以下CbC) の概念を
-取り入れた記法で記述された Agda \cite{agda} のことである．
+しかし,仕様の形式化とその検証には膨大なコストを要する．
+そのため，他のプログラミング言語と比べて検証に適している Gears Agda を使用する．
+Gears Agda とは当研究室で開発している Continuation based C \cite{cbc-gcc}(以下CbC) の概念を取り入れた記法で記述された Agda \cite{agda} のことである．
 
 通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する．
 この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了し，
 メインルーチンに戻る際にスタックしていた環境に戻す流れとなる．
-CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができ，環境をスタックに保持しない．
+CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができる。そのため、環境をスタックに保持しない．
 したがって関数の実行では暗黙な環境が存在せず，関数は受け取った引数のみを使用する．
 この関数の単位を Code Gear と呼び，Code Gearの引数を Data Gear と呼んでいる．
 
 これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている．
 
-先行研究\cite{ryokka-sigos}では,Gears Agda での並列実行の検証について課題が残っていた.
+また、先行研究\cite{ryokka-sigos}では,Gears Agda での並列実行の検証について課題が残っていた.
 並列実行の検証を定理証明で行うには,考慮する状態の数が膨大になり困難である.
 そのため,Gears Agda でモデル検査\cite{EdmundM}を行うことでこの課題に対応する.
 
 CbCの継続の概念はモデル検査とも相性がよい．\cite{ikkun-master}
 CbCが末尾関数呼び出しであるため Code Gear をそのまま
-モデルの edge として定義することができるためである．
+モデルの edge として定義することが可能である．
 
-これらのことから,本論文では,Gears Agda での定理証明とモデル検査について述べる
\ No newline at end of file
+これらのことから,本論文では,Gears Agda での定理証明とモデル検査について述べる。
\ No newline at end of file

--- a/Paper/tex/spin_dpp.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/spin_dpp.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,13 +1,13 @@
 \chapter{Gears Agda によるモデル検査}
 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
-できるが，専門的な知識が多く難易度が高いという欠点がある．
+できる。しかし、専門的な知識が多く難易度が高いという欠点がある．
 加えて,CbCでは並列処理も実行できる\cite{parusu-master}が,
 並列処理を定理証明するには検証する状態が膨大になり困難である.
 そのため,並列処理はモデル検査にて検証する方が良い.
 
 \section{モデル検査とは}
 モデル検査 (Model Cheking) とは,検証手法のひとつである.
-モデル検査はプログラムが入力に対して仕様を満たした動作を
+これはプログラムが入力に対して仕様を満たした動作を
 行うことを網羅的に検証することを指す．
 しかし,モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
 状態爆発が起こり得るという問題がある．

--- a/Paper/tex/tree_desc.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/tree_desc.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,18 +1,18 @@
 \section{Gears Agda における Binary Tree の検証}
 
-ここでは Gears Agda にて 再帰的なデータ構造を検証する例として，
+ここでは Gears Agda にて再帰的なデータ構造を検証する例として，
 Binary Tree \cite{rbtree} を実装・検証する．
 
 \subsection{Gears Agda における木構造の設計}
 
-本研究では，Gears Agda にて Binary Tree の検証を行うにあたり，
+本研究では，Gears Agda にて Binary Tree の検証を行う際に，
 Agda が変数に対して再代入を許していないことが問題になってくる．
 
-そのため下図 \ref{fig:rbt-stack} のように，木構造の root から leaf　に 辿る際に見ているnodeから
-下の　tree をそのまま stack に持つようにする．
+そのため下図 \ref{fig:rbt-stack} のように，木構造の root から leaf に 辿る際に見ているnodeから
+下の tree をそのまま stack に持つようにする．
 
 そして insert や delete を行った後に stack から tree を取り出し，
-元の木構造を再構築 していきながら　rootへ戻る．
+元の木構造を再構築 していきながら rootへ戻る．
 
 \begin{figure}[htpb]
   \begin{center}
@@ -50,25 +50,25 @@
 Agda が追えなくなってしまい，\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう．
 
 そのため関数を新たに定義し，展開したものを受け取り，パターンマッチすることで
-\{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる
+\{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる。
 
 木を stack に入れるのは単純で，操作の対象の key となる varn と
 node のkeyを比較を行う．
-そこからは本来の木構造と同じで，操作の対象の key が小さいなら
+その後、本来の木構造と同じで，操作の対象の key が小さいなら
 left の tree を次の node として遷移する．
 大きいなら right の tree を次の node として遷移していく．
 
 操作の対象となる node に辿り着き，操作を行った後，
 Stack に持っている tree から再構築を行う．
 
-そのコードが Code \ref{bt_replace_impl} となる
+そのコードが Code \ref{bt_replace_impl} となる。
 
 \lstinputlisting[label=bt_replace_impl, caption=Stack から tree を再構築する Code Gear] {src/bt_impl/replace.agda.replaced}
 
 これも Code \ref{bt_find_impl} と同じように構成されており，
-varn と node の key を比較し， vart を List から持ってきた node の どこに加えるかを決めるようになっている．
+varn と node の key を比較し，vart を List から持ってきた node の どこに加えるかを決めるようになっている．
 
-以上の流れを繋げることで， Binary Tree の insert と find を実装できた．
+以上の流れを繋げることで，Binary Tree の insert と find を実装できた．
 delete は insert の値を消すようにすると実装ができる．
 
 \subsection{Gears Agda における Binary Tree の検証}
@@ -80,7 +80,7 @@
 
 \lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced}
 
-この不変条件は， treeInvariant が　tree の 左にある node の key が小さく，
+この不変条件は，treeInvariant が tree の 左にある node の key が小さく，
 右にある node の方が大きいことを条件としている．
 
 stackInvariant は Stack にある tree が，次に取り出す Tree の一部であることを

--- a/Paper/tex/while_loop.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/while_loop.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -2,6 +2,8 @@
 ここでは Gears Agda にて Hoare Logic を用いた検証の例として，
  While Loop プログラムを実装・検証する．
 
+%% ここかその前にinvariantの説明した方がよい？
+
 \subsection{While Loop の実装}
 まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する．
 実装はまず， Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う．
@@ -21,22 +23,21 @@
 \{-$\#$ TERMINATING $\#$-\} のタグを付けると
 停止しないプログラムをコンパイルすることができる
 
-これまでの Code Gear を繋げることで， While Loop　を行う Code を実装することができる．
+これらの Code Gear を繋げることで， While Loop を行う \coderef{while-loop} を実装することができる．
 
-\lstinputlisting[label=while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced}
+\lstinputlisting[label=code:while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced}
 
 \subsection{While Loop の検証}
 
-Gears Agda にて行なった While Loop の実装コードを元に，
-5章にて述べた Pre / Post Condition を記述していくことで
+While Loop の実装コードを元に，前述した Pre / Post Condition を記述していくことで
 Hoare Logic を用いた検証を行う．
 
-検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う．Code \ref{while_verif_init_cg} がそれに当たる．
+検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear から行う．Code \ref{while_verif_init_cg} がそれに当たる．
 
 \lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced}
 
 今回は検証を行いたいため 5.1 で述べたように，実装に加えて Pre / Post Condition を持つ必要がある．
-init時の Pre Condition のみ特殊で　Agda での関数定義の際に記述し，
+init時の Pre Condition のみ特殊で Agda での関数定義の際に記述し，
 「Data Gear に正しく初期値が設定される」という条件を使用する．これが
 ((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10)
 に当たる．
@@ -70,16 +71,16 @@
 
 \lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced}
 
-停止することを Agda が理解できるように記述すると良い．
-そのため引数に減少していく変数 reduce を追加し，
+停止することを Agda が理解できるように記述する．
+そのため引数に減少する変数 reduce を追加し，
 loop するとデクリメントするように実装する．
 
 loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした
 whileLoopSeg を使用する．
 
-そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた．
+そしてこれらを繋げて While Loop の検証を行える\coderef{loop_verif_cg} を実装できた．
 
-\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}
+\lstinputlisting[label=code:loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced}