• OSやアプリケーションの信頼性を高めることは重要な課題である。

• 研究室でCbCという言語を開発している。その信頼性を証明したい。

  • CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。

• プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。

  • CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。

• これらのことから、Hoare Logicを用いてCbCを検証する。

• cbcはサブルーチンとスープ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。

• 先行研究ではCbCにおけるWhileLoopの検証を行なった。

• agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う

# やった事

• モデル検査について調べていた

• Gears Agdaで Red Black Tree を作成する

  • 卒論時に作成していたものを修正するなどしていた
    • deleteの部分に実は上手くできていない所があったのでリファクタリングをしています…
  • 実はもうちょっとでできそうな感じがある。

# モデル検査について

Agdaでモデル検査をする事をkono先生が言っていたので、調べていた

• モデル検査はUnitTestを大量にやる感じの検証手法(ここから調べていた)

• AgdaでNuSMVというものが呼び出せるプラグインを産業技術総合研究所システム検証研究センター作っているみたいだった

• というわけで、nusmvで遊んでいた

  • 昔(b4くらいの時)kono先生が言っていた2*xとx+xの検証してみたかったが、上手く動かせなかった。

• 参考

  • 検証における記述量爆発問題の構造変換による解決
  • Agda プラグイン機構
  • NuSMVによるモデル検査入門 (1)

# 今後やりたい事/やらないといけない事

• while loopの検証
• 研究計画書
  • なぜかアナウンスがまるでない…

# 余談

• M1 MacBook Air でAgda on Spacemacs が動くか検証していた
  • ちゃんと動きました。
  • 過去にemacs plusでAgdaが動くのは確認していた