|
0
|
1 \chapter{Continuation based C と Agda}
|
|
|
2
|
|
2
|
3 本章では当研究室で推奨している単位での検証を行うため、
|
|
|
4 Agda 上で CodeGear、 DataGear の表現を示す。
|
|
|
5 また、Gear の単位と Hoare Logic を対応させ、
|
|
|
6 CbC 上での Hoare Logic について説明を行う。
|
|
|
7
|
|
|
8
|
|
|
9 \section{DataGear と Agda}
|
|
|
10 Agda での DataGear は CodeGear で扱うすべてのデータである。
|
|
|
11
|
|
|
12
|
|
0
|
13
|
|
2
|
14 \section{CodeGear と Agda}
|
|
|
15 CodeGear は DataGear を受け取って処理を行い DataGear を返す。
|
|
|
16 また、CodeGear 間の移動は継続を用いて行われる。
|
|
|
17 継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、
|
|
|
18 次の CodeGear へ継続を行う。
|
|
|
19 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当するため、
|
|
|
20 継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。
|
|
|
21 継続は不定の型 (\verb+t+) を返す関数で表される。
|
|
|
22 CodeGear は次に実行する関数の型を引数として受け取り不定の型\verb+t+を返す関数として記述され、
|
|
|
23 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
|
|
|
24 コード \ref{agda-cg} は Agda で記述した CodeGear の例である。
|
|
0
|
25
|
|
2
|
26 \lstinputlisting[caption= whileTest の型,label=agda-cg]{src/while-test.agda.replaced}
|
|
|
27 %% Agda のとこで Level の話を…！
|
|
|
28 ここでは \verb+c10+ と名付けた自然数を受け取った後、
|
|
|
29 \varb+Env+ を受け取って不定の型\verb+t+を返す関数を受け取り、
|
|
|
30 \verb+t+を返す CodeGear を定義している。
|
|
|
31
|
|
|
32
|
|
|
33
|
|
|
34 \section{Meta CodeGear の表現}
|
|
|
35 Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。
|
|
|
36 Agda での Meta CodeGear は通常の CodeGear を引数に取りそれらの関係などの上位概念を返す CodeGear である。
|
|
|
37 これは(図を入れる)のような Code Gear となる。
|
|
|
38
|
|
|
39 % \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced}
|
|
|
40
|
|
0
|
41
|
|
|
42 \section{CbC 上での HoareLogic の実現}
|
|
2
|
43 CbC 上の Hoare Logic は引数として事前条件、次の CodeGear に渡す値に事後条件を含めることで記述する。
|
|
|
44 その際に事前条件が CodeGear で変更され、事後条件を導く形になる。
|
|
|
45 例として while プログラムの CbC 記述についてみる。
|
|
|
46
|
|
|
47 %% コード
|
|
|
48 ここでは~
|
|
|
49
|
|
|
50 Hoare Logic の記述としてはこれで良く、部分整合性は示せているが、
|
|
|
51 全体の検証を行うためには接続されているすべての CodeGear が実行されたときの健全性(Soundness)が担保される必要がある。
|
|
|
52 そのため、検証用の Meta CodeGear を記述する。
|
|
|
53 例として while プログラムの健全性を担保するプログラムをみる。
|
|
|
54 %% コード
|
|
|
55 このコードでは CodeGear をつなげて終了状態まで実行したとき最後の事後条件が成り立っているため、これらの実行が正しく終了することを示すことができる。
|
