# HG changeset patch # User soto # Date 1613333581 -32400 # Node ID 68485f45c26519fadcbf5e095e25f13f2138ea09 # Parent 1cde48f2323604b9efe33dbe80b30ecd1154446b ADD slide diff -r 1cde48f23236 -r 68485f45c265 paper/final_thesis.pdf Binary file paper/final_thesis.pdf has changed diff -r 1cde48f23236 -r 68485f45c265 paper/tex/future.tex --- a/paper/tex/future.tex Mon Feb 15 03:51:35 2021 +0900 +++ b/paper/tex/future.tex Mon Feb 15 05:13:01 2021 +0900 @@ -18,7 +18,7 @@ 展望としては、Gears Agda コードから CbC コードの変換をしたい。 Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、 -CbC はC言語の下位言語であり、 +CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。 +そのため、Gears Agdaのコードを CbC に変換できるようにしたい。 +これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。 - - diff -r 1cde48f23236 -r 68485f45c265 slide/slide.md --- a/slide/slide.md Mon Feb 15 03:51:35 2021 +0900 +++ b/slide/slide.md Mon Feb 15 05:13:01 2021 +0900 @@ -38,7 +38,13 @@ --- # 証明を用いたプログラムの信頼性の向上を目指す - + +- プログラムの信頼性を高めることは重要な課題である + - 信頼性を高める手法として「モデル検査」や「定理証明」など +- 当研究室でCbCという言語を開発している + - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる +- 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った。 +- 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する --- @@ -47,28 +53,66 @@ - Gears Agda - Gears Agda による Hoare Logic を用いた簡単なプログラムの検証 -- Gears Agda で実装したRed Black Tree +- Gears Agda で実装したRed Black Tree(insert) --- # 今回の成果 - Left Lerning Red Black Tree の実装 -- (delete) 誰もやろうとしていなかった - 証明付き Data 構造を用いた List による性質の記述 --- # Agdaの紹介 +- Agdaとは、定理証明支援器であり、関数型言語である +- 特徴として、変数への再代入が許されていない事や、型を明示する必要がある +```Agda +plus : (x y : N ) → N +plus x zero = x +plus x (suc y) = plus (suc x) y +``` --- -# gears Agda +# Gears Agda +- CbC 実行を継続すると言う仕様に合わせた Agda の記法 +- Env を Data Gear としている +- Env → t を用いる事で次の遷移先を示す +```Agda +plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t +plus-com env next exit with vary env +... | zero = exit (record { varx = varx env ; vary = vary env }) +... | suc y = next (record { varx = suc (varx env) ; vary = y }) +``` --- -# llrbt +# Left Learning Red Black Tree +- Red Black Tree の定義を満たしつつ、実装が用意な Binary Treeの一つ +- 定義は以下である。 + + --- -# delete +# Left Leaning Red Black Tree の実装 +- 通常のプログラミング言語であれば、再代入と再起処理を用いて実装を行う +- Gears Agda では両方行えないため、これらを回避する +- insert / delete をする際に、目的の node まで辿るが、ここで辿った分を +Listに保持する +- 目的の node まで辿った後に、List に保持した node を結合させることで実装を行う + +--- +# 証明付き Data 構造を用いた List による性質の記述 +- Binary Tree の性質も持っているので、大小関係を検証する必要がある +- そこで、証明付き Data 構造を用いた List を下記のように定義した + +--- +# 今後の課題 + +- 作成した Left Learning Red Black Tree を Hoare Logicに当てはめる +- その後、条件の接続ができているのかと、健全性について示す。 --- -# Left Lerning Red Black Tree の実装 +# まとめ ---- +- Left Learning Red Black Tree について記述した +- Meta Data Gear を記述した + - 証明付き Data 構造を用いた List による性質の記述 +- 今後検証に向けて、条件の接続ができているのかと、健全性について示す。