--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2023-01-16.md	Tue Jan 17 00:10:05 2023 +0900
@@ -0,0 +1,45 @@
+# 研究目的
+
+- 形式手法という開発手法がある
+    - プログラムの仕様を形式化し、書いたプログラが仕様を満たしているかを検証しながら開発を行う手法
+    - 安全性や信頼性が重要な場合に使われることが多い
+        - 自動車の組み込みプログラムとか、ロケット開発とかに使われている
+    - 欠点として、検証に膨大なコストがかかる
+- 他のプログラミング言語と比べて検証に適している Gears Agda を検証手法に使う
+    - Gears Agda とは、当研究室で開発しているContinuation based C (CbC) の概念を取り入れた記法で書かれたAgdaのこと
+        - 通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する
+        - この際、メインルーチンで使用していた変数などの環境はスタックされる。サブルーチンが終了しメインルーチンに戻る際にスタックしていた環境を戻す流れ
+        - CbCの場合はサブルーチンコールの際にアセンブラでいうjmp命令により関数遷移をおこなうことができる
+        - つまり、環境をスタックに保持しない。
+        - したがってCbCでは関数の実行では暗黙の環境が存在せず、関数は受け取った引数のみを使用する
+
+    - 定理証明によるプログラムの検証は一般的に難易度が高いが、これにより証明を Code Gear 単位に分割することができる。そのため他プログラミング言語と比べて比較的容易に検証を行えるようになっている
+
+- しかし、定理証明だけでは並列処理の検証は困難となる。
+    - 出てくるパターンすべてに対して定理証明を行うのは現実的ではない
+
+- そのため、もう一つの代表的な検証手法であるモデル検査を Gears Agda で行えるようにした
+    - Code Gear が受け取った Code Gear をもとに実行する点と関数実行後に帰ってこない点により、Code Gearをそのままモデルのedgeとして定義することができるため、Gears Agdaはモデル検査との相性も良い
+
+- これらのことから、Gears Agda での定理証明とモデル検査による検証手法を確立させる
+
+
+
+
+# 今週やったこと
+- State Listの作成やってました
+    - まだちょっとバグがあるっぽい
+- wslでManjaroを立ち上げて、wslgでspacemacsを動かしてagdaをやるなどしていた
+    - 特殊文字が見たことない文字化けをしていて直すのに若干手間取った
+
+## State List の作り方
+
+- Dining Philosophers Problem (以下DPP) の状態に分岐が発生するのはThinking, Eatingの部分
+    - そのため、分岐が発生する際に分岐先を全探索する search_branch 関数
+- 分岐後に1step実行するための step 関数
+- 同じ状態が生成されていた場合にそれを除外するexclude same state 関数
+
+(一つのStateを分岐させたら、そのStateから発生する状態を見たということでdone flagを立てる。これをすべてのStateで実行した際に State List を終了する)
+
+これらをAgda上で　TERMINATING loop で回すことで状態を全部網羅して State List を作成している
+