\chapter{まとめと今後の課題}
\label{c:conclusion}

本論文では Continuation based C プログラムに対して
Hoare Logic をベースにした仕様記述を行った。
また、 implies を用いて状態遷移を記述することで CbC 上での Hoare Logic の健全性を示すことができた。

実際に、 Hoare Logic ベースの記述を行うことで、
検証のメタ計算に使われる Meta DataGear や、
CodeGear の概念、 CbC 上での Pre Condition、
Post Conditionの記述方法が明確になった。

また、検証時に任意の回数ループする Meta CodeGear が存在するとき、
任意の自然数回ループしても正しく次の状態に遷移できることを証明することで、
証明が記述できることが判明した。

さらに、本来の Hoare Logic では決められたコマンドのみでのプログラム記述と検証を行っていたが、
CodeGear をベースにすることでより柔軟な単位でのプログラム記述し、
実際に検証を行えることが分かった。


\section{今後の課題}
今後の課題として、他のループが発生するプログラムの検証が挙げられる。
同様に検証が行えるのであれば、共通で使えるライブラリのような形でまとめることで、
より容易な検証ができるようになるのではないかと考えている。

現在、検証が行われていないループが存在するプログラムとして、
Binary Tree や RedBlack Tree などのデータ構造が挙げられる。

また、Meta DataGear で DataGear の関係等の制約条件を扱うことで、
常に制約を満たすデータを作成することができる。
予めそのようなデータをプログラムを使用することで、検証を行う際の記述減らすことができると考えている。
これも同様に Binary Tree や RedBlack Tree などのデータ構造に適用し、
検証の一助になると考えている。


CodeGear の健全性に関しては、 コマンドが限定されていた Hoare Logic とは異なり、
\verb/implies/ を用いて CodeGear に対してそれぞれの遷移系を記述する必要がある。
これらの遷移系は Meta CodeGear として記述できているため、仕様記述から変換できる形になることが期待できる。


現在の CbC では、検証の記述を Agda で記述しているため、実際の実行に向く記述ではない。
そのため、検証を行った Agda 上の CbC 記述から Agda を用いて、
より高速に実行できる CbC プログラムの生成を行う必要がある。

また、 CbC で開発、検証したいと考えている GearsOS には並列構文が存在しており、
どのように並列動作に対しての検証も課題として挙げられる。