スライド 1

2011/07/05 ICSE 勉強会
担当：新原敦介
Yi Wei 他, Chair of Software Engineering, ETH Zurich, Switzerland, ICSE2011
Inferring Better Contracts
•
背景
– ソフトウェアの信頼性には、ミスを避けるための contracts:制約が効果的
– 静的アプローチでは保守的な制約しかえられず、小さいプログラムしか適用できない
– 動的アプローチではスケーラビリティはあるものの、
既存の手法は sophisticated な性質を導出できない. ← 目的: ここを導出したい
•
提案手法
– Object指向言語 Eiffel を対象
– 既存のAutoTest(著者の成果)を用いた動的アプローチ
– 制約の生成には、３つのアプローチ
• Basic template
• Quantified expressions
• Implication expressions
基本的なテンプレートを用意して、全部試す.
マイニングパターンを用意して、全部試す.
ディシジョンツリーを作りながら、学習する.
sophisticated
– すべてをEiffelでツール化済み
•
評価実験
– 手法： Eiffel Base のデータ構造クラス6個すべてを、提案手法のツールにかける
– 結果： 1283個の制約を生成.
• 正当性 94%
• 完全性 75 %
生成された制約が意味があるものか.
抜け漏れはないか.
⇒ 提案手法の有効性を確認した.
Method Over View
Pre-defined template ※2
- Equalities
- Liner relations
[10]M.D.Ernst他、 Dynamically discovering likely
program invariants to support program evolution
Figure 1 より引用
AutoTest
Eiffel
class
Change Analysis
Test
suite
Change
profile
Random Testing Frameworkで
さまざまなTestを生成
[24]Y.Wei他, Programs that test
themselves. IEEE Software , 2009
Testを実行しValue Setsを作成 ※1
- pre set
- post set
- change set
Predicate
mining
Basic
templates
Validation
Quantified
expressions
Validation
Inferred
contracts
Decision tree
learning
Implication
expressions
Yi Wei 他, Inferring
Confidence
filtering
Better Contracts, ICSE2011
Example: LINKED_LIST.extend
Listing 1 より引用
1. extend ( v: G) -- Add ‘v’ to end . Do not move cursor.
2.
ensure
3.
-- Programmer-written
4.
post_1:
occurrences (v) = old (occurrences(v)) + 1
5.
6.
-- Automatically inferred
7.
post_2:
count = old count + 1
8.
post_3:
i_th (old count + 1 ) = v
9.
post_4:
forall i.
10.
1 < i < old count
implies i_th(i) = old i_th(i)
11.
post_5:
old after
implies index = old index + 1
12.
post_6:
not old after
implies index = old index
13.
14.
post_7:
last = v
15.
post_8:
forall o:G ≠ v.
16.
occurrences(o) = old occurrences(o)
17.
post_9:
forall o:G ≠v.
has(o) = old has(o)
Yi Wei 他, Inferring
basic
Quantified
Quantified
Implication
Implication
basic
Quantified
Quantified
Better Contracts, ICSE2011
Method Detail
たぶん喋れない
Quantified
expressions
forall:
forall o もしくは forall o ≠v について、以下を探す.
x(o) ＝ y(o)
x(o) ≠y(o)
x(o) or y(o) implies z(o)
x(o) and y(o) implies z(o)
vは、入力,
x,y,z は、テスト対象が持つクエリ.
例
LINKED_LIST.extend(v) では、
post_8:
forall o:G ≠ v.
occurrences(o) = old occurrences(o)
post_9:
forall o:G ≠v. has(o) = old has(o)
Sequence-based contracts:
コンテナクラスの中でも、シーケンスなクラスを対象に、
以下のconstractsが存在するか探す.
forall m< j < n.
en(j) = (old en) ( j - m + old m)
en( v + 1) = z
forall v + 1 + σz < j < v + 1 + σz + old ( M - y)
en( j ) = (old en) ( j - v - 1 - σz + old y)
例
LINKED_LIST.extend(v) では、
post_3:
i_th (old count + 1 ) = v
post_4:
forall i.
1 < i < old count
implies i_th(i) = old i_th(i)
Implication
expressions
Decision tree learning:
以下のような木を学習
Figure 3 より引用
old after
False
True
index = old index + 1
index = old index
old after
extendする前のコンテナクラスの、カーソルが、
最終行に来ているか？
True : index = old index + 1
extend 後のカーソルは、extend前からインクリメントする
False : index = old index
extend後のカーソルは、extend前と変わらない
Yi Wei 他, Inferring
Better Contracts, ICSE2011
Experiments
冗長性
EiffelBaseのすべてのデータ構造クラスを対象
自動生成数
入力したクラスの
開発者が書いた数
Table 1 より引用
完全性
正当性(人力)
Repetition
Variation
Auto?
LOC
#CMD
#QRY
#PRE
#POST
#INF
%SND
%CMP
%V
%R
%A
ARRAY
1463
15
32
69
107
235
94
66
80
0
74
HASH_TABLE
2021
14
36
49
102
200
94
50
74
8
22
LINKED_LIST
2000
26
34
70
91
378
98
84
76
2
74
LINKED_QUEUE
2099
6
20
78
94
61
96
100
62
2
84
LINKED_SET
2352
19
37
99
101
294
88
68
68
2
36
LINKED_STACK
2088
9
18
78
94
115
96
100
68
0
100
12023
89
177
373
589
1283
94
75
72
2
56
Class
TOTAL
正答でないケース
LINKED_LIST の merge_left
old is_equal (other) implies is_empty
AutoInfer では、空リスト以外は、リスト
のインスタンスを複数生成しない
Variation: 冗長でも価値がある OK
Repetation:同じ事を表現する NG
Auto?: 開発者が書いたPostConditionが
自動生成とかぶった率
完全性が下がるケース
Setに、意味が付加されると厳しい
例：Hashに、既に存在する
要素を追加するとき
Yi Wei 他, Inferring Better Contracts, ICSE2011

Download Report