Mercurial > hg > Papers > 2016 > atton-ipsjpro

annotate presentation/slide.md @ 51:68b4b3313703

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix slides
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 02 Aug 2016 17:56:27 +0900
parents 9d8b37748b1e
children 02e5ae71c319
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Continuation based C を用いたプログラムの検証手法
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: 比嘉健太
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
3 profile: 琉球大学 大学院 理工学研究科 情報工学専攻
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
6 # ソフトウェアの実装の信頼性の向上
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 * ソフトウェアの信頼性を向上させたい
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
8 * 信頼性を向上させる手法には証明、モデル検査、テストなど様々な手法がある
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
9 * ソフトウェアが定められた仕様を常に満たすか確認することで信頼性を保証する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
10 * 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの実装コードの検証を行なう
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
12 # ソフトウェアの信頼性向上手法
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
13 * アルゴリズムの正しさを証明する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
14 * Agda, Coq, Idris といった証明支援系でプログラムを記述する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
15 * TeX: アルゴリズムの証明をドキュメントとして記述している
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
16 * ソフトウェアの仕様を記述し、その反例が無いかをチェックする
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
17 * Spin, NuSMV, CBMC といったモデルチェッカ
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
18 * テストデータを入力して正しい出力を返すか
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
19 * ユニットテスト
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
20 * assert や型システム、検証用の実行処理系
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
21 * Java Path Finder, Virtual VM, Valgrind
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
23 # ソフトウェアの実装を検証したい
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
24 * アルゴリズムの正しさが証明できても実装する際にバグが入ることがある
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
25 * 単語の打ち間違いによるバグ
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
26 * 同じアルゴリズムを検証と実装で二度記述する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
27 * 検証と実装で言語も違うことも
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
28 * 実際に動作するソフトウェアの実装をチェックしたい
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
29 * 実装コードを変更せずに仕様を保証する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
30 * 実装部分と検証部分も同じ言語で記述したい
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
32 # Continuation based C (CbC)
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
33 * 当研究室で開発している言語
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
34 * 関数呼び出しは末尾のみ、の制約を持ったC言語
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
35 * Tail Call を言語仕様として持つ
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
36 * スタックは持たない
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
37 * goto で飛んで戻ってこない
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
38 * アーキテクチャに依存しないアセンブラ
50
9d8b37748b1e Add images
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
39 * C function を呼ぶこともできる
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
40 * 組込みシステムやOSの記述を目的としている
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
41 * Code Segment, Data Segment という単位でソフトウェアを記述する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
42
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
43 # Code Segment: 処理の単位
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
44 * 単一 Code Segment ではループを含まないシンプルな処理のみを行なう
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
45 * Code Segment どうしを接続してソフトウェア全体を構築していく
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
46 * 依存のない Code Segment どうしは並列に実行することが可能
50
9d8b37748b1e Add images
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
47 ![cs](./images/code_segments.svg){:width="50%"}
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
49 # Data Segment: データの単位
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
50 * Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
51 * Output Data Segment は接続先の Code Segment の Input になる
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
52 * Code Segment 内部で扱う変数は Data Segment に格納される
50
9d8b37748b1e Add images
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
53 ![csds](./images/code_segment_data_segment.svg){:width="50%"}
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 # Example of Code Segment in CbC
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
56 * Code Segment は `__code` を付けた関数
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
57 * 次の Code Segment への接続は `goto` で表される
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 __code addTen(int a) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 int b = a+10;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 goto twice(b);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 __code twice(int x) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 int y = 2*x;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 goto showValue(y);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 # Example of Data Segment in CbC
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
72 * 各 Code Segment で使うデータの構造体の共用体で表現される
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 union Data {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 struct Count {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 int x;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 } count;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 struct Port {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 int port;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 } port;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 };
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
85
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
86 # メタ計算による階層化
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
87 * CbC で書いた実装を CbC で検証していく
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
88 * 仕様記述も CbC で行なう
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
89 * 仕様のチェックも CbC で行なう
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
90 * 実装の記述は変更したくない
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
91 * どこまでがソフトウェア本体でどこまでが実装コード?
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
92 * メタ計算で計算を階層化することで解決する
51
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
93 * 実装はノーマルレベル、検証はメタレベル
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
94 * メタからノーマルは見えて、ノーマルからメタは見えない
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
95
51
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
96 # 階層化のメリット
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
97 * メモリ管理などの検証が難しい部分もメタレベルで行なう
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
98 * 検証するべきノーマルレベルはシンプルになる
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
99 * ノーマルレベルではポインタが出てこない
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
100 * メモリ管理アルゴリズムの切り替えも楽になる
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
101
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
102 # Examples of Meta Computation
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
103 * 計算を実現するような計算
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
104 * プログラムを生成するようなプログラム
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
105 * TemplateHaskell in Haskell, Template in C++, Generics
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
106 * コンパイル時メタプログラミング
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
107 * 言語が特別な API を提供する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
108 * method_missing, define_method in Ruby
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
109 * プログラムがその言語処理系の挙動を変える
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
110 * reflection in Java
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
111 * 副作用などの言語処理系に依存した処理を表現する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
112 * Monad in Haskell
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
113
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
114 # Meta Code Segment
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
115 * メタ計算は Code Segment の接続部分に Meta Code Segment を入れることで表現できる
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
116 * 仕様定義、仕様検証は Meta Code Segment に記述
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
117 * 実装である Code Segment の検証を行なえば良い
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
118 * Input Data Segment を作成して正しい Output Data Segment を出すかチェックする
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
119
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
120 # Meta Data Segment
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
121 * Meta Code Segment に必要なデータを格納する
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
122 * Data Segment より上位の Data Segment
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
123
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
124
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
125 # Code of Meta Computation in Continuation based C
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 * メタ計算は Code Segment の間に挟まれた Code Segment で行なう
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
127 * 例: Data Segment を指定する Meta Code Segment `twice_stub`
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 * ノーマルレベルからはポインタは見えないものとする
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 // Code Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 __code addTen(union Data* ds, int a) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 int b = a+10;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 goto twice_stub(ds);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 // Meta Code Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 __code twice_stub(union Data* ds) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 goto twice(ds->count.x);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 // Code Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 __code twice(int x) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 int y = 2*x;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 goto showValue(y);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 # Meta Computation Hook in CbC
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 * goto する時に必ず通る Meta Code Segment `meta` を作る
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 * `meta` を切り替えることでノーマルレベルの計算を拡張する
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 // Meta Data Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 struct Context {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 union Data *data; // Data Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 unsigned int gotoCount; // メタ計算に必要なデータ
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 unsigned int stepOfAddTen;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 };
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 // Meta Code Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 __code meta(struct Context* context, enum Code next) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 countext.gotoCount++;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 /* 接続時に行なうメタ計算を記述 */
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 switch (next) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 case AddTen:
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 // 特定のCode Segmentへのメタ計算
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 context.stepOfAddTen++;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 goto addTen_stub(context);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 case Twice:
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 goto twice_stub(context);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 // Code Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 __code addTen(struct Context* context, int a) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 x = x+10;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 goto meta(context, Twice);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 // Code Segment
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 __code twice(struct Context* context, int x) {
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 x = x*2;
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 goto meta(context, ShowValue);
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 }
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187 ```
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 # Verification Method of Programs Using Continuation based C
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 * メタ計算として検証機構を導入する
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
191 * 仕様は常に成り立つべき式としてCbCで記述する
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 * 仕様を満たさない Input Data Segment が無いかチェックしていく
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193 * 検証の対象として CbC で記述された赤黒木を用いる
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 # Red-Black Tree
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 * 赤黒木とは木構造のデータ構造
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 * 各ノードに赤と黒の色を割り当て、その色を用いて木のバランスを取る
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 * 赤黒木の条件:
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 * 各ノードは赤または黒の色を持つ
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200 * ルートの色は黒である
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202 * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204 # Verification of Red-Black Tree
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205 * 仕様: 最も長い経路は最も短い経路の高々2倍に収まる
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206 * どのような順番で要素が挿入されても常に仕様が満たされることを確認する
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 * 仕様を満たさないような挿入順番があればそれを表示する
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
208 * 木への挿入は有限の個数だけ行なわれる
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
209
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
210 # Verification Library Akasha
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
211 * 本研究で作成した検証用メタ計算ライブラリ
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
212 * 実装コードの ``meta`` を上書きするだけで検証を行なうことができる
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
213 * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
214 * 挿入後の木はきちんとバランスしているかチェックする
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 * Meta Data Segment に挿入順番や実行履歴を記憶させる
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217 # C Bounded Model Checker
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
218 * Carnegie Mellon University で開発されている ANSI-C の記号実行モデルチェッカ
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
219 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
220 * Red-Black Tree を C に変換して検証
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
221 * 挿入順番は非決定的な入力 `nondet_int` を使う
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
223 # Result of Verification
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224 * CbC のメタ計算 Akasha では要素数13個までチェックできた
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
225 * CBMC ではチェックできなかった
51
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
226
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
227 | | akasha | CBMC |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
228 |----------------------------------|:------:|:----:|
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
229 | 要素数1個までは仕様を保証 | 可 | 不可 |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
230 | 要素数13個までは仕様を保証 | 可 | 不可 |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
231 | 実装にバグを入れた際に反例を表示 | 可 | 不可 |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
232
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
233
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
234 # Comparison of tools
51
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
235
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
236 | | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
237 |------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:|
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
238 | 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 必要 | 必要なし | 必要なし | 必要なし |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
239 | 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
240 | 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
241 | メモリリークなどの検出 | 今は不可能 | 不可能? | 不可能 | | | | 可能 |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
242 | 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | ものによる | 可能 | |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
243 | 反例の表示 | 可能 | 可能 | 不可能 | | | 不可能 | |
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
244
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
245
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
246 # Conclusion and Future Works
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
247 * CBMC では検証できない範囲の検証を行なうことができた
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
248 * 動作するプログラムの記述を変更することなく検証を行なえた
51
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
249 * テストケースの自動生成+仕様の反例表示ができた
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
250 * 今後の課題
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
251 * 挿入だけでなく削除を含む赤黒木の仕様検証
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
252 * 状態の抽象化による探索の効率化
49
49ea5b9d5f67 Update presentation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 48
diff changeset
253 * ポインタへの不正アクセス検出などの機能
51
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
254 * 言語処理系に検証を行ないやすくする機構の導入
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
255
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
256 # TODO: おまけ
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
257 * cbmc のバージョン、オプション
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
258 * rbtree の行数
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
259 * 実行時間
68b4b3313703 Fix slides
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 50
diff changeset
260
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
261
50
9d8b37748b1e Add images
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 49
diff changeset
262
48
0995b4fe3023 Add presentation slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
263 <!-- vim: set filetype=markdown.slide: -->