# HG changeset patch
# User autobackup
# Date 1675091405 -32400
# Node ID 5f712e09cf8aac88d64efd1cc4a4b467e351934e
# Parent  07ae5cfe75bc076855829f00c229f115b9277a5f
backup 2023-01-31

diff -r 07ae5cfe75bc -r 5f712e09cf8a user/soto/log/2023-01-30.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2023-01-30.md	Tue Jan 31 00:10:05 2023 +0900
@@ -0,0 +1,47 @@
+# 研究目的
+
+- 形式手法という開発手法がある
+    - プログラムの仕様を形式化し、書いたプログラが仕様を満たしているかを検証しながら開発を行う手法
+    - 安全性や信頼性が重要な場合に使われることが多い
+        - 自動車の組み込みプログラムとか、ロケット開発とかに使われている
+    - 欠点として、検証に膨大なコストがかかる
+- 他のプログラミング言語と比べて検証に適している 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 での定理証明とモデル検査による検証手法を確立させる
+
+
+
+
+# やったこと
+- 論文の執筆進めてました
+- 修論審査の日程を決めました
+
+## 論文の執筆について
+- だいたい書いたような…？
+- 序論が怪しいので修正中です。
+
+## 修論審査の日程を決めました
+- 2/7の15時~16時になりました。
+
+
+# 今週やること
+- 修論を書ききる
+    - 金曜日くらいには主査副査の先生に投げたいお気持ち
+
+- 修論審査で使うスライドを用意する
+
+- 2/10に事務に投げる書類を書く