--- a/paper/chapter/01-introduction.tex	Tue Feb 02 12:23:46 2021 +0900
+++ b/paper/chapter/01-introduction.tex	Tue Feb 02 14:17:05 2021 +0900
@@ -15,7 +15,7 @@
 
 
 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
-形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。
+形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。
 証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
 Curry-Howard同型対応則により、型と論理式の命題が対応する。
 この型を導出するプログラムと実際の証明が対応する。

--- a/paper/chapter/02-cbc.tex	Tue Feb 02 12:23:46 2021 +0900
+++ b/paper/chapter/02-cbc.tex	Tue Feb 02 14:17:05 2021 +0900
@@ -53,7 +53,7 @@
 \section{メタ計算}
 プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。
 関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}
-OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。
+OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。\cite{Yang:2010:SLI:1806596.1806610}
 
 CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。
 メタ計算で使われるこれらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。

--- a/paper/chapter/04-interface.tex	Tue Feb 02 12:23:46 2021 +0900
+++ b/paper/chapter/04-interface.tex	Tue Feb 02 14:17:05 2021 +0900
@@ -43,12 +43,52 @@
 変更後の構文ではのちのジェネリクス導入のことを踏まえて、\texttt{Type}キーワードは削除した。
 
 
+
 構文を変更するには、 GearsOSのビルドシステム上でInterfaceを利用している箇所を修正する必要がある。
 Interfaceはgenerate\_stub.plで読み込まれ、 CodeGearと入出力のDataGearの数え上げが行われる。
 この処理はInterfaceのパースに相当するものである。
 当然ではあるが、パース対象のInterfaceの構文は、変更前の構文にしか対応していない。
 
 
+\section{Implementの型定義ファイルの導入}
+Interfaceを使う言語では、 Interfaceが決まるとこれを実装するクラスや型が生まれる。
+GearsOSもInterfaceに対応する実装が存在する。
+例えばStack Interfaceの実装はSingleLinkedStackであり、 Queueの実装はSingleLinkedQueueやSynchronizedQueueが存在する。
+
+このSynchronizedQueueはGearsOSではDataGearとして扱われる。
+このDataGearの定義は、 Interfaceの定義のように型定義ファイルが存在するわけではなかった。
+従来はcontext.hのDataGearの宣言部分に、構造体の形式で表現したものを手で記述していた。(ソースコード\ref{src:singleContext.h})
+\lstinputlisting[label=src:singleContext.h, caption=cotnext.hに直接書かれた型定義]{src/singleContext.h}
+
+CbCファイルからはcontext.hをインクルードすることで問題なく型を使うことが可能であるが、 型定義ファイルの存在の有無がInterfaceと実装で異なってしまっていた。
+Perlのトランスコンパイラであるgenerate\_stub.plはInterfaceの型定義ファイルをパースしていた。
+Implementの型も同様に定義ファイルを作製すれば、generate\_stub.plで型定義を用いた様々な処理が可能となり、ビルドシステムが柔軟な挙動が可能となる。
+また型定義は一貫して\texttt{*.h}に記述すれば良くなるため、 プログラマの見通しも良くなる。
+本研究では新たにImplementの型定義ファイルを考案する。
+
+GearsOSではすでにInterfaceの型定義ファイルを持っている。
+Implementの型定義ファイルも、 Interfaceの型定義ファイルと似たシンタックスにしたい。
+Implementの型定義ファイルで持たなければいけないのは、 どのInterfaceを実装しているかの情報である。
+この情報は他言語ではInterfaceの実装を持つ型の宣言時に記述するケースと、型名の記述はせずに言語システムが実装しているかどうかを確認するケースが存在する。
+Javaでは\texttt{implements}キーワードを用いてどのInterfaceを実装しているかを記述する。\cite{javaimpl}
+ソースコード\ref{src:javaimpl}では、\texttt{Pig}クラスは\texttt{Animal} Interfaceを実装している。
+\lstinputlisting[label=src:javaimpl, caption=JavaのImplementキーワード]{src/java-interface-implements.java}
+golangではInterfaceの実装は特にキーワードを指定せずに、 そのInterfaceで定義しているメソッドを、Implementに相当する構造体がすべて実装しているかどうかでチェックされる。
+これはgolangはクラスを持たず、構造体を使ってInterfaceの実装を行う為に、 構造体の定義にどのInterfaceの実装であるかの情報をシンタックス上書けない為である。
+GearsOSでは型定義ファイルを持つことができるために、 golangのような実行時チェックは行わず、 Javaに近い形で表現したい。
+
+導入した型定義でSynchronizedQueueを定義したものをソースコード\ref{src:syncqueue}に示す。
+大まかな定義方法はInterface定義のものと同様である。
+違いとして\texttt{impl}キーワードを導入した。
+これはJavaの\texttt{implements}に相当する機能であり、 実装したInterfaceの名前を記述する。
+現状のGearsOSではImplが持てるInterfaceは1つのみであるため、\texttt{impl}の後ろにはただ1つの型が書かれる。
+型定義の中では独自に定義したCodeGearを書いてもいい。
+これはJavaのプライベートメソッドに相当するものである。
+特にプライベートメソッドがない場合は、 実装側で所持したい変数定義を記述する。
+SynchronizedQueueの例では\texttt{top}などが実装側で所持している変数である。
+\lstinputlisting[label=src:syncqueue, caption=SynchronizedQueueの定義ファイル]{src/SynchronizedQueue.h}
+従来context.hに直接記述していたすべてのDataGearの定義は、 スクリプトで機械的にInterfaceおよびImplementの型定義ファイルに変換している。
+
 \section{Implementの型をいれたことによる間違ったGearsプログラミング}
 Implementの型を導入したが、 GearsOSのプログラミングをするにつれていくつかの間違ったパターンがあることがわかった。
 自動生成されるStubCodeGearは、 goto metaから遷移するのが前提であるため、 引数をContextから取り出す必要がある。

Binary file paper/master_paper.pdf has changed

--- a/paper/reference.bib	Tue Feb 02 12:23:46 2021 +0900
+++ b/paper/reference.bib	Tue Feb 02 14:17:05 2021 +0900
@@ -3,6 +3,11 @@
     howpublished = {\url{https://github.com/josharian/impl}},
 }
 
+@misc{javaimpl,
+    title = {Java implements Keyword},
+    howpublished = {\url{https://www.w3schools.com/java/ref_keyword_implements.asp}},
+}
+
 @misc{eclipse.jdt.ls,
     title = {Eclipse JDT Language Server},
     howpublished = {\url{https://github.com/eclipse/eclipse.jdt.ls}},

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/SynchronizedQueue.h	Tue Feb 02 14:17:05 2021 +0900
@@ -0,0 +1,5 @@
+typedef struct SynchronizedQueue <> impl Queue {
+  struct Element* top;
+  struct Element* last;
+  struct Atomic* atomic;
+} SynchronizedQueue;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/java-interface-implements.java	Tue Feb 02 14:17:05 2021 +0900
@@ -0,0 +1,17 @@
+// interface
+interface Animal {
+  public void animalSound(); // interface method (does not have a body)
+  public void sleep(); // interface method (does not have a body)
+}
+
+// Pig "implements" the Animal interface
+class Pig implements Animal {
+  public void animalSound() {
+    // The body of animalSound() is provided here
+    System.out.println("The pig says: wee wee");
+  }
+  public void sleep() {
+    // The body of sleep() is provided here
+    System.out.println("Zzz");
+  }
+}
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/singleContext.h	Tue Feb 02 14:17:05 2021 +0900
@@ -0,0 +1,24 @@
+union Data {
+   /* 略 */
+    // Queue Interface
+    struct Queue {
+        union Data* queue;
+        union Data* data;
+        enum Code whenEmpty;
+        enum Code clear;
+        enum Code put;
+        enum Code take;
+        enum Code isEmpty;
+        enum Code next;
+    } Queue;
+    struct SingleLinkedQueue {
+        struct Element* top;
+        struct Element* last;
+    } SingleLinkedQueue;
+    struct SynchronizedQueue {
+        struct Element* top;
+        struct Element* last;
+        struct Atomic* atomic;
+    } SynchronizedQueue;
+   /* 略 */
+};