|
3
|
1 \section{検証手法}
|
|
8
|
2 現在提案している手法は、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
|
|
4
|
3 コマンドの部分的な正当性を導けることを前述した。
|
|
|
4 その為、agdaでのcbcの検証は下図のようになる。
|
|
|
5 流れを説明すると、
|
|
|
6 CodeGear の引数となる DataGear が事前条件となり、
|
|
|
7 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。
|
|
|
8 その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。
|
|
3
|
9
|
|
|
10 \subsection{CbC記法で書くagda}
|
|
|
11 CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。
|
|
|
12 以下が例となるコードである。
|
|
4
|
13
|
|
|
14 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda}
|
|
|
15
|
|
3
|
16 前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
|
|
|
17 これがAgdaで表現された CodeGear となる。
|
|
|
18
|
|
|
19 \subsection{agda による Meta Gears}
|
|
|
20 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
|
|
|
21 今回はその Meta Gears をagdaによる検証の為に用いる。
|
|
|
22
|
|
4
|
23 \begin{itemize}
|
|
7
|
24 \item Meta DataGear \mbox{}\\
|
|
|
25 Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
|
|
|
26 これを用いることで、仕様となる制約条件を記述することができる。
|
|
|
27
|
|
|
28 \item Meta CodeGear\mbox{}\\
|
|
|
29 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
|
|
|
30 である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
|
|
|
31 す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
|
|
4
|
32 \end{itemize}
|
|
3
|
33
|
|
4
|
34 \subsection{Code Gear の 遷移の検証}
|
|
|
35 これまで述べた手法にて、CodeGear の検証をすることができる。
|
|
|
36 しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。
|
|
|
37 % また、各 CodeGear が正しく停止することも重要である。
|
|
3
|
38
|
|
4
|
39 遷移の検証のために implies という data 型を導入する。
|
|
|
40 \lstinputlisting[label=implies, caption=implies] {src/implies.agda}
|
|
|
41 これにより CodeGear が正しく遷移できることを検証する。
|
|
3
|
42
|
