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

形式手法入門
VDM++チュートリアル
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
1
目的
n 世界的に成功したほとんどの形式手法仕様システムは、以下
の導入方法で成功している。
参考資料:　IPA形式手法適用調査 調査概要資料
l https://www.ipa.go.jp/files/000004548.pdf)
l １週間程度のセミナー受講
l 経験ある専門家のコンサルティング
n
n 今回のチュートリアルは、上記導入方法の肝を紹介すること
で形式手法導入のための基礎知識を得ることを目的としてい
る。具体的には、
l 実用的な仕様例である運賃計算モデル(現実の仕様の100分の1モデル)
を紹介し、
l そこで使用している重要で頻繁に使用するVDM++言語要素を紹介し、
l 実用的な仕様を作成するための基本を紹介する。
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
2
目次
n 形式手法の概要
n VDMツールのインストールと設定
l Overture Tools
l VDMTools
n VDM++言語入門
l
l
l
l
簡単な例題を通して説明
モデル化の方法
ツールの使い方と文法
簡単な演習
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
3
セミナー資料一覧
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
n セミナー資料
l 形式手法入門VDM++チュートリアル
n 形式手法入門VDM++チュートリアル.pdf
l Overture Toolsのインストールと設定
n Overture Toolsのインストールと設定(Mac OS X版).pdf
n Overture Toolsのインストールと設定(Windows版) .pdf
l 演習解答
n 後ほど配布
l 運賃計算モデル
n Fare0.zip
n 参考資料
l 対象を如何にモデル化するか? (形式記述サンプル付き)
l SEC-FM1-B-1対象を如何にモデル化するか.pdf
l How2MakeModel.zip
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
4
形式手法の概要
n 形式手法(正式手法?)
l 特定の数学モデルに基づく形式言語を用い、記述の曖昧さを除去し、分析や検証を容易に
することにより、高品質ソフトウェアを効率よく開発するための手法
n 形式手法の種類
l モデル規範型
n システムの内部構造の構成的定義をデータや操作を用いてモデル化し検証する
n 種類:　VDM, RAISE（VDM+OBJ+CSP的仕様）, B, Z
n 従来のプログラミングに近い考えなので、現場の技術者に理解しやすい
l 性質規範型
n システムを外部から見た性質を公理や抽象データ型を用いてモデル化し検証する
n 種類:　CafeOBJ, Maude,...
n 代数を使うため抽象度が高く、モデル規範型より現場に適用するのはやや難しい
l モデル検査
n システムの振舞仕様に対し可能な実行パターンを網羅的かつ自動的に検証する
n 種類:　SPIN, SMV,...
n 採用する意味は場合によって大きいが、システム全体をモデル化できない
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
5
なぜ厳密な仕様（形式仕様）でモデル化するか？
n 日本語仕様で大規模システムを記述するのはコストが掛かる
から!
l 形式仕様で「モデル」を記述し検証するほうが、高品質で生
産性が高いから!
n 形式仕様の方が技術移転が容易だから!
n 形式仕様の方が仕様修正が容易だから!
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
6
なぜ厳密な仕様としてVDM（ウィーン開発手法）を採用したか？
n 形式手法の種類
n モデル規範型
n VDM, RAISE（最初に勉強した手法で、VDM+OBJ+CSP的仕様）, B, Z
n 現場の技術者に理解しやすいので採用
n 性質規範型
n CafeOBJ（最初にツールを使用したのが、OBJ3）, Maude,...
n まだ現場に適用するには時期尚早
n モデル検査
n SPIN, SMV,...
n 採用する意味はあるが、現場の技術者にはやや難しい
n 形式手法の検証方法とツール
n 証明
実用までに5年
n 段階的洗練
n RAISE Tool, Rodin
n 採用する意味はあるが、現場の技術者にはかなり難しい
実用までに3年
n モデル検査
n 仕様実行
n VDMTools
実用までに3ヶ月
n 現場の技術者に理解しやすく、形式検証の第一歩として採用
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
7
日本での、形式手法による仕様作成の成果例
(1) SCSK
(2) フェリカネ
ットワークス
対象システム
適用工程
仕様規模
証券業務
実システム
UseCaseレベル
要求仕様
3+3万行
おサイフケータイ・
ファームウェア
モバイルFelica
ICチップ
第２世代
実システム
API外部仕様
欠陥数 生産性
開発
期間
備考
0
2.5倍
45%
開発チームに
業務知識無し
0
2倍
85%
開発チームに
仕様+テストケース
7.4+6.6万行
形式手法知識無し
仕様+テストケース
EAL4+
実システム
API外部仕様
5.5万行
EAL5+予定
FeliCa ICチップ
(RC-SA00)
第3世代
実システム
API外部仕様
同上+
第3世代基本部分は同一
VDM 1.7万行+
EAL6+
(3) 産業技術総 鉄道関係
合研究所,
駅務システム
オムロン
データ
既存システム
厳密仕様
作成実験
モバイルFeliCa
ICチップ
第３世代
SONY
Promela 0.45万行
Copyright © 2016 IPA, All Rights Reserved
0.75+80万行
仕様+テストデータ
欠陥
発見数
29
「暗黙知は
仕様の欠陥」
Software Reliability Enhancement Center
8
目次
n ✔形式手法の概要
n VDMツールのインストールと設定
l Overture Tools
l VDMTools
n VDM++言語入門
l
l
l
l
簡単な例題を通して説明
モデル化の方法
ツールの使い方と文法
簡単な演習
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
9
VDMツールのインストールと設定
n Overture Tools
l インストールと設定
n Mac OS X
l 後述: Overture Toolsのインストールと設定(Mac OS X版)
n Windows
l 後述: Overture Toolsのインストールと設定(Windows版)
n VDMTools
l Mac OS X
n The VDM++ Toolbox-9.0.6-64bit.pkg をダブルクリック
l Windows
n setuppp-9.0.6-i586.exe　をダブルクリック
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
10
Overture Toolsのインストールと設定(Mac OS X版) 実行環境
▾☐㹋遤橆㞮
▾☐KBWB
▾☐+BWBSVOUJNFFOWJSPONFOU+3&
ծ+BWB4&⟃ָ꣬䗳銲կ
• ☐http://www.oracle.com/technetwork/java/javase/
downloads/jre8-downloads-2133155.html
▾☐ًٌٔ٦
• ☐㹋遤⚥‫ך‬0WFSUVSF5PPMT‫ًٌٔך‬⢪欽ꆀ‫כ‬.#
• ☐.BD049‫ؕך‬٦‫(דֽ׌ٕط‬#ַ‫(׵‬#ֻ‫׾ְ׵‬⢪ֲ
‫דך‬ծ(#ًٌٔ٦‫ך‬.BDJOUPTI‫כ‬剑⡚ꣲ䗳銲‫ה‬䙼‫׷׸׻‬կ
▾☐‫ؙأ؍ر‬
• ☐0WFSUVSFBQQ،‫؛ٔف‬٦‫ّء‬ٝ‫כؤ؎؟ؙأ؍رך‬.#
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
11
Overture Toolsのインストールと設定(Mac OS X版) インストール
▾☐؎ٝ‫زأ‬٦ٕ
▾☐http://overturetool.org/download/
•☐0WFSUVSFNBDPTYDPDPBY@[JQխ‫׾‬
‫ל׸ؙׅحؙٕٔـت‬ծずׄ‫تٕؓؿ‬٦‫ח‬
0WFSUVSFBQQָ⡲䧭ׁ‫דך׷׸‬ծ‫׾׸׉‬،‫ٔف‬
‫؛‬٦‫ّء‬ٝ‫تٕؓؿ‬٦‫ח‬獳⹛‫ל׸ׅ‬ծ؎ٝ‫زأ‬٦
ٕ‫כ‬㸣✪կ
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
12
Overture Toolsのインストールと設定(Mac OS X版) 環境設定
▾ ☐0WFSUVSF5PPMT‫ך‬橆㞮鏣㹀
⟃♴‫ך‬鏣㹀⟃㢩‫כ‬ծ⥜姻‫גֻז׃‬葺ְ‫׆כ‬կ
▾ ☐(FOFSBM
▾ ☐"QQFBSBODF
▾ ☐$PMPSTBOE'POUT
•☐‫ؓؿ‬ٝ‫ָز‬㼭ְׁ㜥さ‫כ‬ծֿֿ‫ד‬ծぐ‫ؓؿ‬ٝ‫&׾ؤ؎؟ךز‬EJU‫ג׃‬鏣㹀‫׷ׅ‬
▾ ☐&EJUPST
▾ ☐5FYU&EJUPST
•☐4IPXMJOFOVNCFST‫׷ؙׅحؑث׾‬կ
▾ ☐8PSLTQBDF
▾ ☐5FYUMFFODPEJOH
▾ ☐0UIFS
•☐65'‫׾‬鼅䫛
▾ ☐7%.
▾ ☐5IF7%.5PPMCPYW.PO.BSխ‫ך‬鏣㹀
▾ ☐4$4,7%.5PPMT
•☐1BUIUP7%.5PPMTGPS7%.11WQQHEF
奋‫ח‬ծ"QQMJDBUJPOT5IF7%.5PPMCPYCJO‫׾‬鏣㹀
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
13
Overture Toolsのインストールと設定(Mac OS X版) プロジェクト設定
▾☐‫زؙؑآٗف‬鏣㹀
▾☐1SPQFSUJFT鏣㹀
‫׾زؙؑآٗف‬鼅䫛‫׃‬ծ$POUSPM䊩‫ؙحؙٔ‬
〸‫ؙحؙٔ‬湱䔲‫ג׃‬1SPQFSUJFT‫׾‬鼅䫛‫׷ׅ‬
▾☐7%.4FUUJOHT‫׾‬鼅䫛‫׷ׅ‬
▾☐-BOHVBHFPQUJPOT
▾☐-BOHVBHFWFSTJPO
•☐DMBTTJD‫כزٕؓؿ؍ر‬WEN
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
14
Overture Toolsのインストールと設定(Windows版) 実行環境
▾☐㹋遤橆㞮
▾☐KBWB
▾☐+BWBSVOUJNFFOWJSPONFOU+3&
ծ+BWB4&⟃ָ꣬䗳銲կ
• ☐ http://www.oracle.com/technetwork/java/javase/downloads/jre8-
downloads-2133155.html
▾☐ ًٌٔ٦
• ☐㹋遤⚥‫ך‬0WFSUVSF5PPMT‫ًٌٔך‬⢪欽ꆀ‫כ‬.#
• ☐(#ًٌٔ٦‫ך‬8JOEPXT‫ءو‬ٝ‫כ‬剑⡚ꣲ䗳銲‫ה‬䙼‫׷׸׻‬կ
▾☐ ‫ؙأ؍ر‬
• ☐PWFSUVSFFYF،‫؛ٔف‬٦‫ّء‬ٝ‫כؤ؎؟ؙأ؍رך‬.#玎䏝
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
15
Overture Toolsのインストールと設定(Windows版) インストール
▾☐؎ٝ‫زأ‬٦ٕ
▾☐ http://overturetool.org/download/
•☐ 0WFSUVSFXJOXJOY[JQխ‫׾‬
‫؎ל׸ؙׅحؙٕٔـت‬ٝ‫زأ‬٦ٕ‫כ‬㸣
✪կ
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
16
Overture Toolsのインストールと設定(Windows版) Preference設定
▾ ☐0WFSUVSF5PPMT‫ך‬1SFGFSFODF鏣㹀0WFSUVSF5PPMT‫ך‬8JOEPXً‫ُص‬٦ַ‫׵‬鼅䫛
⟃♴‫ך‬鏣㹀⟃㢩‫כ‬ծ⥜姻‫גֻז׃‬葺ְ‫׆כ‬կ
▾ ☐(FOFSBM
▾ ☐"QQFBSBODF
▾ ☐$PMPSTBOE'POUT
•☐‫ؓؿ‬ٝ‫ָز‬㼭ְׁ㜥さ‫כ‬ծֿֿ‫ד‬ծぐ‫ؓؿ‬ٝ‫&׾ؤ؎؟ךز‬EJU‫ג׃‬鏣㹀‫׷ׅ‬
▾ ☐&EJUPST
▾ ☐5FYU&EJUPST
•☐4IPXMJOFOVNCFST‫׷ؙׅحؑث׾‬կ
▾ ☐8PSLTQBDF
▾ ☐5FYUMFFODPEJOH
▾ ☐0UIFS
•☐65'‫׾‬鼅䫛
▾ ☐7%.
▾ ☐5IF7%.5PPMCPYW.PO.BSխ‫ך‬鏣㹀
▾ ☐4$4,7%.5PPMT
▾ ☐1BUIUP7%.5PPMTGPS7%.11WQQHEF
奋‫ח‬ծWQQHEFFYF‫׾أػך‬鏣㹀
▾ ☐7%.5PPMT‫כ‬鸐䌢ծ⟃♴‫تٕؓؿך‬٦‫؎ח‬ٝ‫زأ‬٦ׁٕ‫׷׸‬
•☐$=1SPHSBN'JMFT=5IF7%.5PPMCPYW=CJO=WQQHEFFYF
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
17
Overture Toolsのインストールと設定(Windows版) プロジェクト設定
▾☐‫زؙؑآٗف‬鏣㹀
▾☐1SPQFSUJFT鏣㹀
‫׾زؙؑآٗف‬鼅䫛‫׃‬ծ〸‫ג׃ؙحؙٔ‬1SPQFSUJFT‫׾‬鼅䫛‫׷ׅ‬
▾☐7%.4FUUJOHT‫׾‬鼅䫛‫׷ׅ‬
▾☐-BOHVBHFPQUJPOT
▾☐-BOHVBHFWFSTJPO
• ☐DMBTTJD‫כزٕؓؿ؍ر‬WEN
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
18
目次
n ✔形式手法の概要
n ✔VDMツールのインストールと設定
l ✔Overture Tools
l ✔VDMTools
n VDM++言語入門
l
l
l
l
簡単な例題を通して説明
モデル化の方法
ツールの使い方と文法
簡単な演習
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
19
n VDM++言語入門
n 集合を使った運賃表から運賃を求めるVDM++モデルFare0の紹介
l Overture ToolsのView
l Fare0のプロジェクトを読み込む
l 運賃表クラス定義と型定義
l 運賃表集合の型定義
l 「運賃表を検索する」関数
l 「運賃表集合に存在する」か判定する関数
l 運賃計算クラス
l 「運賃を得る」操作(operation)
l テストケースの作成: 簡易回帰テスト
l 組み合わせ(Combinatorial)テスト
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
20
集合を使った運賃表から運賃を求めるVDM++モデルFare0の紹介
要求辞書階層
業務論理階層
テストケース階層
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
21
Overture ToolsのView
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
22
Overture ToolsでFare0のプロジェクトを読み込む
n workspaceを切り替える(switch)
l Fileメニュー -> Switch workspace -> Other…
n Fare0を含むフォルダーをworkspaceに指定する
n Welcomeウィンドウを閉じる
n VDM Explorer viewで
l Fileメニュー -> New -> Project から、
n Select WizardからVDM-PP Projectを選択し、
l Project nameにFare0を設定してFinishボタンを押す
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
23
Overture ToolsにFare0フォルダーが表示される
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
24
FareTable.vdmppを選択するとエディタに表示
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
25
Fare0プロジェクトの確認:
Fare0モデルの簡易回帰テスト
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
26
Overture Toolsから、VDMToolsの起動確認
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
27
VDMToolsによる組み合わせテストの確認
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
28
Overture Toolsによる組み合わせテストの確認
Window -> Open Perspective -> Other... -> Combinatorial Testing メニュー
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
29
運賃表クラス定義と型定義
class 運賃表 --運賃表クラスを定義する。
types --型定義
LM 4.2.2 列型
public 駅 = seq of char
--文字型の列、すなわち文字列。ここでは、駅型が文字列であると定義する。
--publicは、どのクラスからもアクセスできることを示す。
LM 4.2.2 列型 (空列)
inv w駅 == w駅 <> "";
-- inv以下の不変条件定義で、駅型が空文字列ではないことを定義する。
--‘;’は、文法要素の区切り記号である。
VDM++言語マニュアル(今後LMと略記)
public 運賃 = nat; -- 運賃が自然数型であることを定義する。
4.2.5 レコード型
public 運賃レコード ::
-- f駅1とf駅2とf運賃を項目（欄, fieldとも言う）として持つレコード型「運賃レコード」を定義する。
f駅1 : 駅 --欄名の先頭のfは、他の識別子と区別をするために付けている。
--VDM++では、識別子がモデル内でユニークでならないため、このような名付規則を決めたほうが良い。
f駅2 : 駅
f運賃 : 運賃 --ここは、不変条件定義のinvが続くため、セミコロンを付けると構文エラーになる。
LM 4.3 不変条件 (型の不変条件)
inv --駅1と駅2が異なることを、型不変条件で示している。
w運賃レコード == w運賃レコード.f駅1 <> w運賃レコード.f駅2;
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
30
VDMToolsの実行ウィンドウ
レコード型構成子
LM 4.2.5レコード型
ここに
p mk_運賃表`運賃レコード( a ,"b",130)
を入力
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
31
レコード型インスタンスの表示
レコード構成子の構文
構文: 式= . . .
LM 7.11 レコード式
| レコード構成子
| . . . ;
レコード構成子= ‘mk ’, 名称, ‘(’, [ 式リスト], ‘)’ ;
演習問題: 以下のレコード型インスタンスを、VDMToolsのインタプリタ・
ウインドウで実行するとどうなるかを確かめよ。
print mk_運賃表`運賃レコード( a","b",130)
print mk_運賃表`運賃レコード( a","a",130)
print mk_運賃表`運賃レコード("a","",130)
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
32
運賃表集合の型定義
LM 4.2.1 集合型
public 運賃表集合 = set of 運賃レコード -- 運賃表集合型が、運賃レコード型のデータの集合であることを示す。
-- 集合は、順序がなく、重複がないものの集まりである。
inv w運賃表集合 == -- 型の不変条件invの後の識別子名は、型の値を表す名前で、 "==™ の後の式中で使う。
w運賃表集合 = {} or -- {}は空集合を表す。
forall w運賃レコード1, w運賃レコード2 in set w運賃表集合 &
-- forallは全称限量式で、w運賃表集合の要素、w運賃レコード1と
-- w運賃レコード2が、’&’の後の条件式を満たす事を示す。
LM 7.5 限量式
w運賃レコード1.f駅1 = w運賃レコード2.f駅1 and
-- ここでは、w運賃表集合で駅1と駅2が等しければ、運賃も等しいことを示す。
LM 4.1.1 ブール型
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)};*/
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
33
ブール型含意演算子と集合型演算子
VDMToolsのインタプリタ・ウインドウで、以下を実行する
LM 7.7 集合式 (集合列挙)
とどうなるか?
print 1 in set {3,1,2}
print (1 not in set {3,1,2}) => false
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
34
集合の列挙式と型の不変条件のチェック
集合式の構文
LM 7.7 集合式 (集合列挙)
構文: 式 = . . .
| 集合列挙
|...;
集合列挙 = ‘{’, [ 式リスト], ‘}’ ;
集合の要素の値を返す式
式リスト = 式, { ‘,’, 式} ;
演習問題: VDMToolsのインタプリタ・ウインドウで、以下の運賃表集合列挙式を引数として構成子運賃
計算を実行するとどうなるかを確かめよ。
create c := new 運賃計算(
{mk_運賃表`運賃レコード("東京", "新宿", 180),
mk_運賃表`運賃レコード("新宿", "品川", 190),
mk_運賃表`運賃レコード("新宿", "品川", 300)})
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
35
限量式
n 限量式は、制約に関する仕様の記述に便利な1階述語論理式
l 「全ての〜について〜が成り立つ」を記述するのに全称限量式
l 「〜がなりたつ〜が存在する」を記述するのに存在限量式
l 「〜がなりたつ〜が唯一つ存在する」を記述するのに1存在限量式
l 不変条件(inv)、事前条件(pre)、事後条件(post)で使うことが多い
限量式の構文
LM 7.5 限量式
構文: 式 = . . .
¦ 限量式
¦...;
限量式 = 全称限量式
¦ 存在限量式
¦ 1存在限量式;
全称限量式 = forall , 束縛リスト, & , 式;
存在限量式 = exists , 束縛リスト, & , 式;
束縛リスト = 多重束縛, { , , 多重束縛} ;
1存在限量式 = exists1 , 束縛, & , 式;
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
36
限量式 (全称限量式)
VDMToolsのインタプリタ・ウインドウで、以下を実行する
とどうなるか?
LM 9 束縛 (型束縛)
普通、型束縛は実行できないが、
bool型は{true, false}しか値がないので実行できる
print forall a,b : bool & a => b <=> not a or b
print forall a,b : bool & not (a and b) <=> not a or not b
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
37
限量式 (存在限量式)
VDMToolsのインタプリタ・ウインドウで、以下を実行する
とどうなるか?
LM 7.7 集合式 (集合範囲式)
print exists a,b in set {1,...,9} & a mod 2 = 0
print exists a,b in set {1,...,9} & a+b = 18
print exists a,b in set {1,...,9} & a+b = 19
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
38
限量式 (1存在限量式)
VDMToolsのインタプリタ・ウインドウで、以下を実行する
とどうなるか?
print exists1 a in set {1,...,9} & a mod 2 = 0
print exists1 a in set {1,...,9} & a mod 5 = 0
print exists1 a in set {1,...,9} & 2 * a = 18
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
39
「運賃表を検索する」関数
protected 運賃表を検索する : 運賃表集合 * 駅 * 駅 -> 運賃レコード
--関数「運賃表を検索する」の関数名と引数の型と返値の型を示す。
LM 6 関数定義
--protectedはサブクラスからのみアクセスできることを示す。
運賃表を検索する(a運賃表集合, a駅1, a駅2) ==
--関数「運賃表を検索する」の、仮引数を示す。
LM 7.1 let式 (let be式)
let w運賃レコード in set a運賃表集合 be st
-- let be st式で、a運賃表集合の要素で、次の行の条件式を満たす値が「w運賃レコード」に束縛される。
{a駅1, a駅2} = {w運賃レコード.f駅1, w運賃レコード.f駅2}
--駅1と駅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存在限量式」で、
LM 5 アルゴリズム定義 (予約語RESULT)
--a運賃表集合の要素で'&'の後の条件式を満たす唯1つの要素「w運賃レコード」が存在することを主張する
{a駅1, a駅2} = {w運賃レコード.f駅1, w運賃レコード.f駅2} and
RESULT = w運賃レコード; -- RESULTは、事後条件式の中だけで使える予約後で、返り値の値を示す。
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
40
let be式
構文: 式 = let 式
| let be 式
|...;
let 式 = ‘let’, ローカル定義{ ‘,’, ローカル定義}, ‘in’, 式;
LM 7.1 let式 (let be式)
let be 式 = ‘let’, 束縛, [ ‘be’, ‘st’, 式], ‘in’, 式;
ローカル定義 = 値定義
| 関数定義;
LM 8 パターン
値定義 = パターン, [ ‘:’, 型], ‘=’, 式;
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
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
41
パターン
LM 8 パターン
構文: パターン = パターン識別子
| 一致値
| 集合列挙パターン
| 集合合併パターン
| 列列挙パターン
| 列連結パターン
| 写像列挙パターン
| 写像併合パターン
| 組パターン
| レコードパターン;
パターン識別子 = 識別子 | ‘-’
n パターン
l パターンはある特定の型の1つの値に一
致する。
n パターン識別子
l どんな型のどんな値にも一致する。
l 識別子の場合
n 識別子がその値に束縛される
l don't-care記号'-'の場合
n 束縛は起きない
n 他のパターンは中級以上で使用す
るので、説明しない
識別子 = ( 文字), { ( 文字 | ‘'’ | ‘_’ } ;
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
42
パターン識別子の例
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記号'-'と一致させて、束縛が起きないようにし、
この後使わないようにしている。
*/
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
43
束縛
LM 9 束縛
構文: 束縛 = 集合束縛 | 型束縛;
集合束縛 = パターン, ‘in set’, 式;
型束縛 = パターン, ‘:’, 型;
束縛リスト = 多重束縛, { ‘,’, 多重束縛} ;
多重束縛 = 多重集合束縛
| 多重型束縛;
多重集合束縛 = パターンリスト, ‘in set’, 式;
多重型束縛 = パターンリスト, ‘:’, 型;
n 束縛は、パターンと一致する値の範囲を指定する。
n 集合束縛では、値は集合から選ばれ、
n 型束縛では、値は型から選ばれるので、自然数(nat)型など無限の要素がある型は
実行できない。
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
44
束縛の例
LM 4.2.1 集合型 演算子
有限べき集合(power), 濃度(card)
集合束縛
{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
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
45
「運賃表集合に存在する」か判定する関数
protected 運賃表集合に存在する : 運賃表集合 * 駅 * 駅 -> bool
LM 7.7 集合式 (集合内包)
運賃表集合に存在する(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 運賃表 --運賃表クラスの定義がここで終わることを示す。
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
46
集合内包式
集合式の構文
LM 7.7 集合式 (集合内包)
構文: 式 = . . .
| 集合内包
集合の要素の値を返す式
|...;
式リスト = 式, { ‘,’, 式} ;
集合内包 = ‘{’, 式, ‘|’, 束縛リスト, [ ‘&’, 式], ‘}’ ;
多重集合束縛= パターンリスト, ‘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
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
47
運賃計算クラス
class 運賃計算 is subclass of 運賃表
--運賃計算クラスが運賃表クラスのサブクラスであることを示す。
LM 11 インスタンス変数
instance variables
--インスタンス変数の定義。VDM++では、インスタンス変数のみが広域(グローバル)変数。
s運賃表集合 : 運賃表集合 := {};
--s運賃表集合は、他のクラスからはアクセスできないprivateな運賃表集合型のインスタンス変数で、
--初期値は空集合である。
operations
-- 構成子はクラスのインスタンスを生成する。
{mk_運賃表`運賃レコード("東京", "品川", 220),
mk_運賃表`運賃レコード("東京", "新宿", 180),
mk_運賃表`運賃レコード("新宿", "品川", 190)};
-- 引数なしの構成子は自動的に生成されるので、ここで定義する必要はない。
public 運賃計算 : 運賃表集合 ==> 運賃計算
--構成子の操作名と返り値の型名はクラス名と同じでなければならない。
運賃計算(a運賃表集合) == s運賃表集合 := a運賃表集合;
LM 13.4 代入文
--引数で受け取った内容を、インスタンス変数に代入(記号は":=")する。
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
48
「運賃を得る」操作(operation)
public 運賃を得る : 駅 * 駅 ==> 運賃
--操作「運賃を得る」の操作名と引数の型と返値の型を示す。引数がない場合、返り値がない場合は"()"を使用する。
運賃を得る(a駅1, a駅2) == --操作「運賃を得る」の、仮引数を示す。
let w運賃レコード = 運賃表を検索する(s運賃表集合, a駅1, a駅2) in
LM 13.1 let文
-- let式で、「運賃表を検索する」関数の返り値を「w運賃レコード」に束縛し、
return w運賃レコード.f運賃 -- 運賃レコードのf運賃欄の値をreturn文で返している。 LM 13.10 return文
pre --操作の事前条件。操作の場合、事前条件は受け入れ可能な引数とインスタンス変数であることを保証する。
運賃表集合に存在する(s運賃表集合, a駅1, a駅2)
post --操作の事後条件。操作の事後条件では、インスタンス変数を使用できる。
LM 7.5 1存在限量式
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 運賃計算
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
49
ここまでのまとめ
✔要求辞書階層
✔業務論理階層
テストケース階層
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
50
テストケースの作成: 簡易回帰テスト
class Test is subclass of 運賃計算
--Testクラスが運賃計算クラスのサブクラスであることを示す。
LM 10 値(定数)定義
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]を返す。
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
51
簡易回帰テストの個々のテストケース
operations
public t1 : () ==> bool
--1番目の回帰テストケースの操作。うまく行ったか否かをbool型で返す。
t1() == ( -- '('から')'までが1つのブロック分で、複数の文を記述できる。
LM 13.1 let文
--今は、1つのdef文が記述されていて、その中に、return文が記述されている。
let w運賃計算 = new 運賃計算(v運賃レコード集合) in
-- let式の中で、v運賃レコード集合を持った運賃計算オブジェクトを生成し、w運賃計算に束縛する。
return w運賃計算.運賃を得る("東京", "品川")
= 220
-- w運賃計算の「運賃を得る」をcallし、結果が220であればtrueをreturn文で返す。
);
public t2 : () ==> bool
t2() == (
let w運賃計算 = new 運賃計算(v運賃レコード集合) in
LM 13.3 ブロック文
return w運賃計算.運賃を得る("東京", "新宿") = 180
);
...
end Test
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
52
VDMToolsで簡易回帰テスト
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
53
ここまでのまとめ
✔要求辞書階層
✔業務論理階層
✔テストケース階層
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
54
組み合わせ(Combinatorial)テスト
class UseFare0
values --定数の定義
v運賃レコード集合 : 運賃表`運賃表集合 = { -- 「運賃表`運賃表集合」は、運賃表クラスの運賃表集合を示す。
mk_運賃表`運賃レコード("東京", "品川", 220),
mk_運賃表`運賃レコード("東京", "新宿", 180),
mk_運賃表`運賃レコード("新宿", "品川", 190)
};
instance variables
sTest : Test := new Test();
s運賃計算 : 運賃計算 := new 運賃計算(v運賃レコード集合);
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
55
組み合わせ(Combinatorial)テスト
traces --以下が、組み合わせテストであることを示す。文法が、通常のVDM++ソースと多少異なる。
LM 17 traces定義
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回実行される。*/
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
56
簡単な演習
class 例外処理例 --演習に使う構文の使用例(ExitSample.vdmpp)
operations
public 割る : nat * nat ==> real
割る(n1, n2) ==
if n2 = 0 then
exit <割り算の分母が0である>
LM 13.11 例外処理文 (exit文)
LM 4.1.4 引用型
-- このexit文は、<割り算の分母が0である>という引用型の例外を発生させる。
else
return n1 / n2;
LM 4.2.4 組型 (演習には使わない)
public 例外処理をする : nat * nat ==> bool * real --この返値は、bool型とreal型の組型を返す
例外処理をする(n1, n2) ==
LM 13.11 例外処理文 (trap文)
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 例外処理例
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
57
演習問題1
n 例外処理文を使って、Fare0モデルのエラー処理仕様を記述せよ
l ヒント:
n 業務論理階層のクラス内の操作の事前条件を注釈とし、exit文
でエラーの場合に例外を発生させる文を追加する
l
Fare0モデルの場合、「運賃を得る」操作を修正すれば良い
l
Fare0.vdmppを修正
n 発生する例外の処理をtrap文で記述するクラスを記述する
l
Fare0モデルの場合、回帰テストケースでtrap文を使用して、
意図的に発生させたエラーの例外をキャッチして、trueを返す
テストケースを書けば良い
l
Fare0_testspec.vdmppを修正
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
58
演習問題2
n 演習問題1で修正したFare0モデルをテストするため、組み合
わせテストを修正せよ
l ヒント:
n traces名 T1 にテストデータを追加すれば良い
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
59
まとめ
n 形式手法の導入で成功している導入方法を参考に、実際の
仕様の100分の1モデルを通して、実用的なVDM++仕様を作
成し検証するための基本を紹介した。
n 今回、実際の仕様記述と検証で使用することの多いVDM++
関連の主な機能で紹介できなかったこと:
l 写像型、列型、トークン型、合併型と選択型
l インスタンス変数の不変条件
l 実用的な回帰テストライブラリ
n より詳しい副読本は、以下を参考にしていただきたい。
l
SEC-FM1-B-1 対象を如何にモデル化するか? 形式記述サンプル付き (簡易製本配布)
Copyright © 2016 IPA, All Rights Reserved
Software Reliability Enhancement Center
60
参考: VDMのツール
ツール
開発者
仕様
IDEベース環境
インタープリタ
特徴
Java, C++生成。オブジェクト
VDMTools
SCSK
独自(C++)
独自(Qt使用) 数が多い場合、vdmjより速
い。クラス図生成。
vdmi
Overture
Tools
Vienna Talk
Nick Battle
Fujitsu
Services(英国)
Overture Project
(デンマーク、英国、
オランダ、ポルトガ
ル、日本)
小田朋宏
SRA
Copyright © 2016 IPA, All Rights Reserved
独自(Java)
VDMJのソース
を利用
VDMJをプロ
セス間通信で
利用
IDE無し
オブジェクト数が少ない場合
は、VDMToolsより速い。
Java生成。オブジェクト数が
Eclipse
少ない場合は、VDMToolsより
速い。クラス図生成?
Pharo
Smalltalk
VDM-SL仕様が対象。
Smalltalk生成。
Software Reliability Enhancement Center
61