|
2
|
1 Continuation Based C の Hoare Logic を用いた仕様記述と検証
|
|
|
2 =====
|
|
|
3
|
|
|
4 琉球大学大学院 : 並列信頼研究室\
|
|
|
5 外間 政尊
|
|
|
6
|
|
|
7 ---
|
|
|
8
|
|
|
9 ## OS の検証技術としての Hoare Logic の問題点
|
|
|
10 - OS やアプリケーションの信頼性は重要な課題
|
|
|
11
|
|
|
12 - 信頼性を上げるために仕様の検証が必要
|
|
|
13
|
|
|
14 - 検証にはモデル検査や**定理証明**などが存在する
|
|
|
15
|
|
|
16 - 定理証明では証明の手法と型システムの対応を用いて検証
|
|
|
17
|
|
|
18 - また、仕様検証の手法として **Hoare Logic** がある
|
|
|
19
|
|
|
20 - Hoare Logic ではコマンドを実行する上で事前の条件があり、実行が停止したとき成立する条件がある
|
|
|
21
|
|
|
22 - コマンドが細かいため大きなプログラムを記述するのが大変
|
|
|
23
|
|
|
24 ---
|
|
|
25
|
|
|
26 ## Hoare Logic をベースにした Gears 単位での検証
|
|
|
27 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案している
|
|
|
28
|
|
|
29 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
|
|
|
30
|
|
|
31 - CodeGear は継続を用いて次の CodeGear に接続される
|
|
|
32
|
|
|
33 - **定理証明支援機**である **Agda** 上で CodeGear DataGear の単位を用いた検証を行う
|
|
|
34
|
|
|
35 - 本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する
|
|
|
36
|
|
|
37 ---
|
|
|
38
|
|
|
39 ## Hoare Logic
|
|
|
40 Hoare Logic はプログラム検証の手法
|
|
|
41
|
|
|
42 事前条件( P )が成り立つとき、コマンド( C )を実行すると事後条件( Q )が成り立つ
|
|
|
43
|
|
|
44 これは **{ P } C { Q }** の形で表され、Hoare Triple と呼ばれる
|
|
|
45
|
|
|
46 以下のような while program を検証した
|
|
|
47
|
|
|
48 n = 10 となっているが検証では n は任意の自然数
|
|
|
49
|
|
|
50 ```C
|
|
|
51 n = 10;
|
|
|
52 i = 0;
|
|
|
53
|
|
|
54 while (n>0)
|
|
|
55 {
|
|
|
56 i++;
|
|
|
57 n--;
|
|
|
58 }
|
|
|
59 ```
|
|
|
60
|
|
|
61 ---
|
|
|
62
|
|
|
63 ## Hoare Logic と while program
|
|
|
64
|
|
|
65 **Seq** はコマンドを2つ受け取って順に実行する
|
|
|
66
|
|
|
67 **PComm** は代入
|
|
|
68
|
|
|
69 **while** は変数の状態が(0<n)の間、コマンドを繰り返し実行
|
|
|
70
|
|
|
71 実際に while program を表すために、コマンドでの構文木を記述している
|
|
|
72
|
|
|
73 ```
|
|
|
74 Seq
|
|
|
75 / \
|
|
|
76 PComm Seq
|
|
|
77 (n=10) / \
|
|
|
78 PComm While
|
|
|
79 (i=0) |
|
|
|
80 Cond
|
|
|
81 (0<n)
|
|
|
82 |
|
|
|
83 Seq
|
|
|
84 / \
|
|
|
85 PComm PComm
|
|
|
86 (i++) (n--)
|
|
|
87 ```
|
|
|
88 更にこの後、プログラムの仕様を記述して証明する
|
|
|
89
|
|
|
90 ---
|
|
|
91
|
|
|
92 ## CbC での Hoare Logic 概略
|
|
|
93 CodeGear は処理の単位、更にメタレベルの処理を Meta CodeGear という単位で分けてる
|
|
|
94
|
|
|
95 メタレベルの処理は今見えるところだと CodeGear 間を接続する処理とか
|
|
|
96
|
|
|
97 
|
|
|
98 
|
|
|
99
|
|
|
100 Meta CodeGear で信頼性の検証を行う
|
|
|
101
|
|
|
102
|
|
|
103
|
|
|
104 ## 詳しい話、質問等はポスターで！
|
|
|
105 よろしくお願いします
|
|
|
106
|
|
|
107 ご静聴ありがとうございました
|
|
|
108
|
|
|
109
|
|
|
110 ## CbC での Hoare Logic 記述
|
|
|
111 「代入」、「ループ」の２つの CodeGear に分けた
|
|
|
112
|
|
|
113 代入では「事前条件なし」 から 「n=10 かつ i=0」
|
|
|
114
|
|
|
115 ループでは少し条件を緩めて 「n + i = 10」
|
|
|
116
|
|
|
117 ループ終了後は 「i=0」が成り立ってるはず
|
|
|
118
|
|
|
119 というのを Gears 単位上で Hoare Logic っぽく検証しましたというお話になる予定
|
|
|
120
|
|
|
121 --- |
