形式手法入門VDM++チュートリアル.key

Transcription

1

2 目的 n 世界的に成功したほとんどの形式手法仕様システムは 以下の導入方法で成功している n 参考資料 : IPA 形式手法適用調査調査概要資料 l l 1 週間程度のセミナー受講 l 経験ある専門家のコンサルティング n 今回のチュートリアルは 上記導入方法の肝を紹介することで形式手法導入のための基礎知識を得ることを目的としている 具体的には l 実用的な仕様例である運賃計算モデル ( 現実の仕様の 100 分の 1 モデル ) を紹介し l そこで使用している重要で頻繁に使用する VDM++ 言語要素を紹介し l 実用的な仕様を作成するための基本を紹介する 2

3 目次 n 形式手法の概要 n VDM ツールのインストールと設定 l Overture Tools l VDMTools n VDM++ 言語入門 l 簡単な例題を通して説明 l モデル化の方法 l ツールの使い方と文法 l 簡単な演習 3

4 セミナー資料一覧 n n n マニュアル l VDM++ 演算子要約 n Quick_Overview_of_VDM_Operators_J.pdf l VDMTools VDM++ 言語マニュアル n langmanpp_a4j.pdf l VDMTools ユーザーマニュアル (VDM++) n usermanpp_a4j.pdf l Overture VDM-10 Tool Support: User Guide n OvertureIDEUserGuide.pdf セミナー資料 l l l l 形式手法入門 VDM++ チュートリアル n 形式手法入門 VDM++ チュートリアル.pdf Overture Toolsのインストールと設定 n Overture Toolsのインストールと設定 (Mac OS X 版 ).pdf n Overture Toolsのインストールと設定 (Windows 版 ).pdf 演習解答 n 後ほど配布運賃計算モデル n Fare0.zip 参考資料 l 対象を如何にモデル化するか? ( 形式記述サンプル付き ) l SEC-FM1-B-1 対象を如何にモデル化するか.pdf l How2MakeModel.zip 4

5 形式手法の概要 n 形式手法 ( 正式手法?) n l 特定の数学モデルに基づく形式言語を用い 記述の曖昧さを除去し 分析や検証を容易にすることにより 高品質ソフトウェアを効率よく開発するための手法 形式手法の種類 l モデル規範型 n システムの内部構造の構成的定義をデータや操作を用いてモデル化し検証する n 種類 : VDM, RAISE(VDM+OBJ+CSP 的仕様 ), B, Z n 従来のプログラミングに近い考えなので 現場の技術者に理解しやすい l 性質規範型 n システムを外部から見た性質を公理や抽象データ型を用いてモデル化し検証する n 種類 : CafeOBJ, Maude,... n 代数を使うため抽象度が高く モデル規範型より現場に適用するのはやや難しい l モデル検査 n システムの振舞仕様に対し可能な実行パターンを網羅的かつ自動的に検証する n 種類 : SPIN, SMV,... n 採用する意味は場合によって大きいが システム全体をモデル化できない 5

6 なぜ厳密な仕様 ( 形式仕様 ) でモデル化するか? n 日本語仕様で大規模システムを記述するのはコストが掛かるから! l 形式仕様で モデル を記述し検証するほうが 高品質で生産性が高いから! n 形式仕様の方が技術移転が容易だから! n 形式仕様の方が仕様修正が容易だから! 6

7 なぜ厳密な仕様として VDM( ウィーン開発手法 ) を採用したか? n n 形式手法の種類 n モデル規範型 n VDM, RAISE( 最初に勉強した手法で VDM+OBJ+CSP 的仕様 ), B, Z n 現場の技術者に理解しやすいので採用 n 性質規範型 n CafeOBJ( 最初にツールを使用したのが OBJ3), Maude,... n まだ現場に適用するには時期尚早 n モデル検査 n SPIN, SMV,... n 採用する意味はあるが 現場の技術者にはやや難しい形式手法の検証方法とツール n 証明 n 段階的洗練 n RAISE Tool, Rodin n 採用する意味はあるが 現場の技術者にはかなり難しい n モデル検査 n 仕様実行 n VDMTools n 現場の技術者に理解しやすく 形式検証の第一歩として採用 実用までに 5 年 実用までに 3 年 実用までに 3 ヶ月 7

8 日本での 形式手法による仕様作成の成果例 8

9 目次 n 形式手法の概要 n VDM ツールのインストールと設定 l Overture Tools l VDMTools n VDM++ 言語入門 l 簡単な例題を通して説明 l モデル化の方法 l ツールの使い方と文法 l 簡単な演習 9

10 VDM ツールのインストールと設定 n Overture Tools l インストールと設定 nmac OS X l 後述 : Overture Tools のインストールと設定 (Mac OS X 版 ) nwindows l 後述 : Overture Toolsのインストールと設定 (Windows 版 ) n VDMTools l Mac OS X nthe VDM++ Toolbox bit.pkg をダブルクリック l Windows n setuppp i586.exe をダブルクリック 10

11 Overture Tools のインストールと設定 (Mac OS X 版 ) 実行環境 downloads/jre8-downloads html 11

12 Overture Tools のインストールと設定 (Mac OS X 版 ) インストール 12

13 Overture Tools のインストールと設定 (Mac OS X 版 ) 環境設定 13

14 Overture Tools のインストールと設定 (Mac OS X 版 ) プロジェクト設定 14

15 Overture Tools のインストールと設定 (Windows 版 ) 実行環境 downloads html 15

16 Overture Tools のインストールと設定 (Windows 版 ) インストール 16

17 Overture Tools のインストールと設定 (Windows 版 ) Preference 設定 17

18 Overture Tools のインストールと設定 (Windows 版 ) プロジェクト設定 18

19 目次 n 形式手法の概要 n VDM ツールのインストールと設定 l Overture Tools l VDMTools n VDM++ 言語入門 l 簡単な例題を通して説明 l モデル化の方法 l ツールの使い方と文法 l 簡単な演習 19

20 n VDM++ 言語入門 n 集合を使った運賃表から運賃を求めるVDM++ モデルFare0の紹介 l Overture ToolsのView l Fare0のプロジェクトを読み込む l 運賃表クラス定義と型定義 l 運賃表集合の型定義 l 運賃表を検索する 関数 l 運賃表集合に存在する か判定する関数 l 運賃計算クラス l 運賃を得る 操作(operation) l テストケースの作成 : 簡易回帰テスト l 組み合わせ (Combinatorial) テスト 20

21 集合を使った運賃表から運賃を求める VDM++ モデル Fare0 の紹介 要求辞書 業務論理 テストケース 21

22 Overture Tools の View 22

23 Overture Tools Fare0 n workspaceを切り替える (switch) l Fileメニュー -> Switch workspace -> Other nfare0を含むフォルダーをworkspaceに指定する n Welcomeウィンドウを閉じる n VDM Explorer viewで l Fileメニュー -> New -> Project から nselect WizardからVDM-PP Projectを選択し l Project nameにfare0を設定してfinishボタンを押す 23

24 Overture Tools に Fare0 フォルダーが表示される 24

25 FareTable.vdmpp を選択するとエディタに表示 25

26 Fare0 プロジェクトの確認 : Fare0 モデルの簡易回帰テスト 26

27 Overture Tools から VDMTools の起動確認 27

28 VDMTools による組み合わせテストの確認 28

29 Overture Tools による組み合わせテストの確認 29

30 運賃表クラス定義と型定義 class -- types -- public = seq of char -- --public inv w == w <> ""; -- inv -- ; public = nat; -- public :: -- f 1 f 2 f, field f 1 : -- f --VDM++ f 2 : f : -- inv inv w == w.f 1 <> w.f 2; LM LM ( ) VDM++ ( LM ) LM 4.3 ( ) 30

31 VDMTools の実行ウィンドウ LM

32 レコード型インスタンスの表示 : =... LM ; = mk,, (, [ ], ) ; 32

33 運賃表集合の型定義 LM public = set of inv w == -- inv "== w = {} or -- {} forall w 1, w 2 in set w & -- forall w w 1 -- w 2 & w 1.f 1 = w 2.f 1 and -- w 1 2 w 1.f 2 = w 2.f 2 => -- "=>" bool a => b not a or b w 1.f = w 2.f ; /* {mk_ ` (" ", " ", 180), mk_ ` (" ", " ", 190), mk_ ` (" ", " ", 300)};*/ LM 7.5 LM

34 34

35 集合の列挙式と型の不変条件のチェック : = ; = {, [ ], } ; =, {,, } ; 35

36 n 限量式は 制約に関する仕様の記述に便利な 1 階述語論理式 l 全ての について が成り立つ を記述するのに全称限量式 l がなりたつ が存在する を記述するのに存在限量式 l がなりたつ が唯一つ存在する を記述するのに 1 存在限量式 l 不変条件 (inv) 事前条件 (pre) 事後条件 (post) で使うことが多い LM

37 ( ) LM 9 ( ) bool {true, false} 37

38 ( ) 38

39 (1 ) 39

40 運賃表を検索する 関数 protected : * * -> -- --protected (a, a 1, a 2) == -- let w in set a be st -- let be st a w {a 1, a 2} = {w.f 1, w.f 2} a 1 2 w in w -- w pre -- pre true -- (a, a 1, a 2) post -- post true exists1 w in set a & --exists1 1 --a '&' 1 w {a 1, a 2} = {w.f 1, w.f 2} and RESULT = w ; -- RESULT 40

41 let be 式 : = let let be... ; let = let, {,, }, in, ; let be = let,, [ be, st, ], in, ; = ; =, [ :, ], =, ; VDMTools? p let s1 = {1,...,9} in let w in set s1 be st w mod 3 = 0 in w p let s1 = {1,...,9} in let w in set s1 be st w mod 3 = 0 and w mod 2 = 0 in w p let w in set {1,...,9} in w 41

42 パターン : = ; = - n パターン l パターンはある特定の型の 1 つの値に一致する n パターン識別子 l どんな型のどんな値にも一致する l 識別子の場合 n 識別子がその値に束縛される l don't-care 記号 '-' の場合 n 束縛は起きない n 他のパターンは中級以上で使用するので 説明しない = ( ), { ( ' _ } ; 42

43 パターン識別子の例 let w = (s, a 1, a 2) in -- let w return w.f -- f return public print : seq of char ==> () print(a ) == let - = new IO().echo(a ) in skip; /* IO echo */ false don't-care '-' 43

44 束縛 : = ; =, in set, ; =, :, ; =, {,, } ; = ; =, in set, ; =, :, ; n 束縛は パターンと一致する値の範囲を指定する n 集合束縛では 値は集合から選ばれ n 型束縛では 値は型から選ばれるので 自然数 (nat) 型など無限の要素がある型は実行できない 44

45 束縛の例 {e e in set power {1,...,4} & card e = 2} {e e : bool < > < > < > < >} {{a,b} a in set {1,2,3,4}, b in set {3,4,5,6} & card {a,b} = 2} forall a,b : bool & a => b <=> not a or b 45

46 運賃表集合に存在する か判定する関数 protected : * * -> bool (a, a 1, a 2) == {a 1, a 2} in set {{e.f 1, e.f 2} e in set a }; -- in set true --{{e.f 1, e.f 2} e in set a & {a 1, a 2} = {e.f 1, e.f 2}} <> {}; {{e.f 1, e.f 2} e in set a } '&' -- a e {e.f 1, e.f 2} -- {} ' ' -- '{' ' ' ' ' '}' -- in set e in set S e S -- end -- 46

47 集合内包式 : = ; =, {,, } ; = {,,,, [ &, ], } ; =, in set, ; VDMTools? p {w w in set {1,...,9} & w mod 3 = 0} p {w w in set {1,...,9} & w mod 3 = 0 and w mod 2 = 0} p let w in set {1,...,9} in w 47

48 運賃計算クラス class is subclass of -- instance variables -- VDM++ ( ) s : := {}; --s private -- operations public : ==> -- (a ) == s := a ; -- ( ":=") {mk_ ` (" ", " ", 220), mk_ ` (" ", " ", 180), mk_ ` (" ", " ", 190)}; 48

49 運賃を得る 操作 (operation) public : * ==> -- "()" (a 1, a 2) == -- let w = (s, a 1, a 2) in -- let w return w.f -- f return pre -- (s, a 1, a 2) post -- LM exists1 w in set s & --exists1 1 --s '&' 1 w {a 1, a 2} = {w.f 1, w.f 2} and RESULT = w.f ; end 49

50 ここまでのまとめ 要求辞書 業務論理 テストケース 50

51 テストケースの作成 : 簡易回帰テスト class Test is subclass of --Test values -- v : = { }; -- v mk_ (" ", " ", 220), -- mk_ mk_ (" ", " ", 180), mk_ (" ", " ", 190) operations public run : () ==> seq1 of bool -- bool seq1 run() == return [t1(), t2(), t3()]; -- [true, true, true] -- n n false -- 2 [true, false, true] 51

52 簡易回帰テストの個々のテストケース operations public t1 : () ==> bool --1 bool t1() == ( -- '(' ')' def return ); let w = new (v ) in -- let v w return w. (" ", " ") = w call 220 true return public t2 : () ==> bool t2() == ( let w = new (v ) in );... return w. (" ", " ") = 180 end Test 52

53 VDMTools で簡易回帰テスト 53

54 ここまでのまとめ 要求辞書 業務論理 テストケース 54

55 組み合わせ (Combinatorial) テスト class UseFare0 values -- v : ` = { -- ` }; mk_ ` (" ", " ", 220), mk_ ` (" ", " ", 180), mk_ ` (" ", " ", 190) instance variables stest : Test := new Test(); s : := new (v ); 55

56 組み合わせ (Combinatorial) テスト traces -- VDM++ T0: stest.run() -- ':' trace T1: let w 1 in set {" ", " ", " "} in -- w 1 {" ", " ", " "} let w 2 in set {" ", " ", " ", " ", ""} in ( -- w 2 {" ", " ", " ", " ", ""} s. (w 1, w 2) -- {w 1, w 2} ) /* let w 1 in set {" ", " ", " "} in... VDM++ w 1 {" ", " ", " "} 1 let w 2 in set {" ", " ", " ", " ", ""} in... w 2 " ", " ", " ", " ", ""} 1 traces w 1 3 w 2 5 = 15 (w 1, w 2) 15 */ 56

57 簡単な演習 class -- (ExitSample.vdmpp) operations public : nat * nat ==> real (n1, n2) == if n2 = 0 then exit < 0 > -- exit < 0 > else return n1 / n2; public : nat * nat ==> bool * real -- bool real (n1, n2) == trap < 0 > -- trap in return < 0 > -- mk_(false, -1) with return mk_(false, -1) in return mk_(true, (n1, n2)); -- mk_(true, (n1, n2) ) end 57

58 演習問題 1 n 例外処理文を使って Fare0モデルのエラー処理仕様を記述せよ l ヒント : n 業務論理階層のクラス内の操作の事前条件を注釈とし exit 文でエラーの場合に例外を発生させる文を追加する l Fare0モデルの場合 運賃を得る 操作を修正すれば良い l Fare0.vdmppを修正 n 発生する例外の処理をtrap 文で記述するクラスを記述する l Fare0モデルの場合 回帰テストケースでtrap 文を使用して 意図的に発生させたエラーの例外をキャッチして trueを返すテストケースを書けば良い l Fare0_testspec.vdmppを修正 58

59 演習問題 2 n 演習問題 1 で修正した Fare0 モデルをテストするため 組み合わせテストを修正せよ l ヒント : n traces 名 T1 にテストデータを追加すれば良い 59

60 まとめ n 形式手法の導入で成功している導入方法を参考に 実際の仕様の 100 分の 1 モデルを通して 実用的な VDM++ 仕様を作成し検証するための基本を紹介した n 今回 実際の仕様記述と検証で使用することの多い VDM++ 関連の主な機能で紹介できなかったこと : l 写像型 列型 トークン型 合併型と選択型 l インスタンス変数の不変条件 l 実用的な回帰テストライブラリ n より詳しい副読本は 以下を参考にしていただきたい l SEC-FM1-B-1 対象を如何にモデル化するか? 形式記述サンプル付き ( 簡易製本配布 ) 60

61 参考 : VDM のツール 61