# 研究目的

- 形式手法という開発手法がある
    - プログラムの仕様を形式化し、書いたプログラが仕様を満たしているかを検証しながら開発を行う手法
    - 安全性や信頼性が重要な場合に使われることが多い
        - 自動車の組み込みプログラムとか、ロケット開発とかに使われている
    - 欠点として、検証に膨大なコストがかかる
- 他のプログラミング言語と比べて検証に適している 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 での定理証明とモデル検査による検証手法を確立させる




# やったこと
- 論文の執筆進めてました
    - 現状で書けるところはだいたい書いた気がしています
- SPIN での Dining Philosophers Problem のモデル検査を論文に載せたい
    - 実際にやってみた

## 論文の執筆について
- ページ数がこれ以上増えなさそうな予感がしています
- 卒論と似たり似てなかったりしてます

## SPINでのDPPのモデル検査
- 論文に書きたい(すでに書いている)

# 今週やること
- State List のバグを直す
    - 論文は書いたもの寝かせて熟成させたいと思っています
    - 来週見て完成させたい

- 修論審査の日程を調整する