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

形式手法入門

目的

n

世界的に成功したほとんどの形式手法仕様システムは、以下

の導入方法で成功している。

n

_{参考資料:　IPA形式手法適用調査 調査概要資料}

l

https://www.ipa.go.jp/files/000004548.pdf)

l

１週間程度のセミナー受講

l

経験ある専門家のコンサルティング

n

今回のチュートリアルは、上記導入方法の肝を紹介すること

で形式手法導入のための基礎知識を得ることを目的としてい

る。具体的には、

l

実用的な仕様例である運賃計算モデル(現実の仕様の100分の1モデル)

を紹介し、

l

そこで使用している重要で頻繁に使用するVDM++言語要素を紹介し、

l

実用的な仕様を作成するための基本を紹介する。

目次

n

形式手法の概要

n

VDMツールのインストールと設定

l

Overture Tools

l

VDMTools

n

VDM++言語入門

l

簡単な例題を通して説明

l

モデル化の方法

l

ツールの使い方と文法

l

簡単な演習

セミナー資料一覧

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

形式手法の概要

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

_{採用する意味は場合によって大きいが、システム全体をモデル化できない}

なぜ厳密な仕様（形式仕様）でモデル化するか？

n

日本語仕様で大規模システムを記述するのはコストが掛かる

から!

l

形式仕様で「モデル」を記述し検証するほうが、高品質で生

産性が高い

から!

n

形式仕様の方が技術移転が容易だから!

n

形式仕様の方が仕様修正が容易だから!

なぜ厳密な仕様として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

証明

n

段階的洗練

n

RAISE Tool, Rodin

n

採用する意味はあるが、現場の技術者にはかなり難しい

n

モデル検査

n

仕様実行

n

VDMTools

n

現場の技術者に理解しやすく、形式検証の第一歩として採用

実用までに3ヶ月

実用までに3年

実用までに5年

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

対象システム

適用工程

仕様規模

欠陥数 生産性

開発

期間

備考

(1) SCSK

証券業務

実システム

UseCaseレベル

要求仕様

3+3万行

0

2.5倍

45%

開発チームに

業務知識無し

(2) フェリカネ

ットワークス

SONY

モバイルFelica

ICチップ

第２世代

実システム

API外部仕様

7.4+6.6万行

0

2倍

85%

開発チームに

形式手法知識無し

EAL4+

第３世代

実システム

API外部仕様

5.5万行

EAL5+予定

FeliCa ICチップ

(RC-SA00)

第3世代

実システム

API外部仕様

同上+

VDM 1.7万行+

EAL6+

(3) 産業技術総

合研究所,

オムロン

鉄道関係

駅務システム

データ

既存システム

厳密仕様

作成実験

0.75+80万行

欠陥

発見数

29

「暗黙知は

仕様の欠陥」

目次

n

✔形式手法の概要

n

VDMツールのインストールと設定

l

Overture Tools

l

VDMTools

n

VDM++言語入門

l

簡単な例題を通して説明

l

モデル化の方法

l

ツールの使い方と文法

l

簡単な演習

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　をダブルクリック

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

▾

☐
㹋遤橆㞮

▾

☐
KBWB

▾

☐
+BWB
SVOUJNF
FOWJSPONFOU
+3&
ծ+BWB
4&

⟃ָ꣬䗳銲կ

•

☐
http://www.oracle.com/technetwork/java/javase/

downloads/jre8-downloads-2133155.html

▾

☐
ًٌٔ٦

•
☐
㹋遤⚥ך0WFSUVSF
5PPMTךًٌٔ⢪欽ꆀכ.#

•
☐
.BD
04
9ךؕ٦طٕ׌ֽד(#ַ׵(#ֻ׵ְ׾⢪ֲ

ךדծ(#ًٌٔ٦ך.BDJOUPTIכ剑⡚ꣲ䗳銲ה䙼׻׸׷կ

▾

☐
ر؍أؙ

•
☐
0WFSUVSFBQQ،فٔ؛٦ءّٝךر؍أؙ؟؎ؤכ

.#

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

▾

☐
؎ٝأز٦ٕ

▾

☐
http://overturetool.org/download/

•
☐
0WFSUVSFNBDPTYDPDPBY@[JQխ׾

تـؙٕٔحؙׅ׸לծずׄؿٕؓت٦ח

0WFSUVSFBQQָ⡲䧭ׁ׸׷ךדծ׉׸׾،فٔ

؛٦ءّٝؿٕؓت٦ח獳⹛ׅ׸לծ؎ٝأز٦

ٕכ㸣✪կ

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

▾

☐
0WFSUVSF
5PPMTך橆㞮鏣㹀

⟃♴ך鏣㹀⟃㢩כծ⥜姻׃זֻג葺ְכ׆կ

▾

☐
(FOFSBM

▾

☐
"QQFBSBODF

▾

☐
$PMPST
BOE
'POUT

•

☐
ؿؓٝزָ㼭ְׁ㜥さכծֿֿדծぐؿؓٝزך؟؎ؤ׾&EJU׃ג鏣㹀ׅ׷

▾

☐
&EJUPST

▾

☐
5FYU
&EJUPST

•

☐
4IPX
MJOF
OVNCFST
׾ثؑحؙׅ׷կ

▾

☐
8PSLTQBDF

▾

☐
5FYU
MF
FODPEJOH

▾

☐
0UIFS

•

☐
65'׾鼅䫛

▾

☐
7%.

▾

☐
5IF
7%.
5PPMCPY
W

.PO
.BS

խך鏣㹀

▾

☐
4$4,7%.5PPMT

•

☐
1BUI
UP
7%.
5PPMT
GPS
7%.11 WQQHEF奋חծ"QQMJDBUJPOT5IF7%.5PPMCPYCJO
׾鏣㹀

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

▾

☐
فٗآؙؑز鏣㹀

▾

☐
1SPQFSUJFT鏣㹀

فٗآؙؑز׾鼅䫛׃ծ$POUSPM䊩ؙٔحؙ

〸ؙٔحؙ湱䔲׃ג1SPQFSUJFT׾鼅䫛ׅ׷

▾

☐
7%.
4FUUJOHT׾鼅䫛ׅ׷

▾

☐

-BOHVBHF
PQUJPOT

▾

☐
-BOHVBHF
WFSTJPO

•

☐
DMBTTJDر؍ؿٕؓزכWEN

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

▾

☐
㹋遤橆㞮

▾

☐
KBWB

▾

☐
+BWB
SVOUJNF
FOWJSPONFOU
+3&
ծ+BWB
4&

⟃ָ꣬䗳銲կ

•

☐
http://www.oracle.com/technetwork/java/javase/downloads/jre8-downloads-2133155.html

▾

☐
ًٌٔ٦

•
☐
㹋遤⚥ך0WFSUVSF
5PPMTךًٌٔ⢪欽ꆀכ.#

•
☐
(#ًٌٔ٦ך8JOEPXTوءٝכ剑⡚ꣲ䗳銲ה䙼׻׸׷կ

▾

☐
ر؍أؙ

•
☐
PWFSUVSFFYF،فٔ؛٦ءّٝךر؍أؙ؟؎ؤכ.#玎䏝

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

▾

☐
؎ٝأز٦ٕ

▾

☐

http://overturetool.org/download/

•
☐
0WFSUVSFXJOXJOY[JQխ׾

تـؙٕٔحؙׅ׸ל؎ٝأز٦ٕכ㸣

✪կ

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

▾

_{☐
0WFSUVSF
5PPMTך1SFGFSFODF鏣㹀 0WFSUVSF
5PPMTך8JOEPXًصُ٦ַ׵鼅䫛}

⟃♴ך鏣㹀⟃㢩כծ⥜姻׃זֻג葺ְכ׆կ

▾

_☐
(FOFSBM

▾

_{☐
"QQFBSBODF}

▾

_{☐
$PMPST
BOE
'POUT}

•

☐
ؿؓٝزָ㼭ְׁ㜥さכծֿֿדծぐؿؓٝزך؟؎ؤ׾&EJU׃ג鏣㹀ׅ׷

▾

_☐
&EJUPST

▾

_{☐
5FYU
&EJUPST}

•

☐
4IPX
MJOF
OVNCFST
׾ثؑحؙׅ׷կ

▾

_{☐
8PSLTQBDF}

▾

_{☐
5FYU
MF
FODPEJOH}

▾

_☐
0UIFS

•

☐
65'׾鼅䫛

▾

_☐
7%.

▾

_{☐
5IF
7%.
5PPMCPY
W

.PO
.BS

խך鏣㹀}

▾

_{☐
4$4,7%.5PPMT}

▾

_{☐
1BUI
UP
7%.
5PPMT
GPS
7%.11 WQQHEF奋חծWQQHEFFYF
ךػأ׾鏣㹀}

▾

_{☐
7%.5PPMTכ鸐䌢ծ⟃♴ךؿٕؓت٦ח؎ٝأز٦ׁٕ׸׷}

•

☐
$=1SPHSBN
'JMFT=5IF
7%.
5PPMCPY
W=CJO=WQQHEFFYF

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

▾

☐
فٗآؙؑز鏣㹀

▾

☐
1SPQFSUJFT鏣㹀

فٗآؙؑز׾鼅䫛׃ծ〸ؙٔحؙ׃ג1SPQFSUJFT׾鼅䫛ׅ׷

▾

☐
7%.
4FUUJOHT׾鼅䫛ׅ׷

▾

☐
-BOHVBHF
PQUJPOT

▾

☐
-BOHVBHF
WFSTJPO

•

☐
DMBTTJDر؍ؿٕؓزכWEN

目次

n

✔形式手法の概要

n

✔VDMツールのインストールと設定

l

✔Overture Tools

l

✔VDMTools

n

VDM++言語入門

l

簡単な例題を通して説明

l

モデル化の方法

l

ツールの使い方と文法

l

簡単な演習

n

VDM++言語入門

n

集合を使った運賃表から運賃を求めるVDM++モデルFare0の紹介

l

Overture ToolsのView

l

Fare0のプロジェクトを読み込む

l

運賃表クラス定義と型定義

l

運賃表集合の型定義

l

「運賃表集合に存在する」か判定する関数

l

運賃計算クラス

l

「運賃を得る」操作(operation)

l

テストケースの作成: 簡易回帰テスト

l

組み合わせ(Combinatorial)テスト

l

「運賃表を検索する」関数

集合を使った運賃表から運賃を求めるVDM++モデルFare0の紹介

テストケース階層

業務論理階層

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を選択し、

Fare0プロジェクトの確認:

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

運賃表クラス定義と型定義

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

--駅1と駅2が異なることを、型不変条件で示している。

VDM++言語マニュアル(今後LMと略記)

4.2.5 レコード型

LM 4.3 不変条件 (型の不変条件)

LM 4.2.2 列型

LM 4.2.2 列型 (空列)

VDMToolsの実行ウィンドウ

ここに

p mk_運賃表`運賃レコード( a ,"b",130)

を入力

レコード型構成子

LM 4.2.5レコード型

レコード型インスタンスの表示

演習問題: 以下のレコード型インスタンスを、VDMToolsのインタプリタ・

ウインドウで実行するとどうなるかを確かめよ。

print mk_運賃表`運賃レコード( a","b",130)

print mk_運賃表`運賃レコード( a","a",130)

print mk_運賃表`運賃レコード("a","",130)

レコード構成子の構文

構文: 式= . . .

|

レコード構成子

     | . . . ;

レコード構成子= ‘mk ’,

名称

_{, ‘(’, [}

式リスト

_{], ‘)’ ;}

LM 7.11 レコード式

運賃表集合の型定義

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 4.2.1 集合型

LM 7.5 限量式

LM 4.1.1 ブール型

含意演算子

ブール型含意演算子と集合型演算子

VDMToolsのインタプリタ・ウインドウで、以下を実行する

とどうなるか?

print 1

in set

{3,1,2}

print (1

not in set

{3,1,2}) => false

集合の列挙式と型の不変条件のチェック

演習問題: VDMToolsのインタプリタ・ウインドウで、以下の運賃表集合列挙式を引数として構成子運賃

計算を実行するとどうなるかを確かめよ。

create c := new 運賃計算(

{mk_運賃表`運賃レコード("東京", "新宿", 180),

mk_運賃表`運賃レコード("新宿", "品川", 190),

mk_運賃表`運賃レコード("新宿", "品川", 300)})

集合式の構文

構文: 式 = . . .

|

集合列挙

| . . . ;

集合列挙 = ‘{’, [

式リスト

_{], ‘}’ ;}

式リスト =

式

_{, { ‘,’,}

式

_{} ;}

LM 7.7 集合式 (集合列挙)

集合の要素の値を返す式

限量式

n

限量式は、制約に関する仕様の記述に便利な1階述語論理式

l

「全ての〜について〜が成り立つ」を記述するのに全称限量式

l

「〜がなりたつ〜が存在する」を記述するのに存在限量式

l

「〜がなりたつ〜が唯一つ存在する」を記述するのに1存在限量式

l

不変条件(inv)、事前条件(pre)、事後条件(post)で使うことが多い

限量式の構文

構文: 式 = . . .

¦

限量式

¦ . . . ;

限量式 =

全称限量式

¦

存在限量式

¦

1存在限量式

;

全称限量式 = forall ,

束縛リスト

, & ,

式

;

存在限量式 = exists ,

束縛リスト

, & ,

式

;

束縛リスト =

多重束縛

, { , ,

多重束縛

} ;

LM 7.5 限量式

限量式 (全称限量式)

VDMToolsのインタプリタ・ウインドウで、以下を実行する

とどうなるか?

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

LM 9 束縛 (型束縛)

普通、型束縛は実行できないが、

限量式 (存在限量式)

VDMToolsのインタプリタ・ウインドウで、以下を実行する

とどうなるか?

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

限量式 (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

「運賃表を検索する」関数

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}

--駅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存在限量式」で、

--a運賃表集合の要素で'&'の後の条件式を満たす唯1つの要素「w運賃レコード」が存在することを主張する

{a駅1, a駅2} = {w運賃レコード.f駅1, w運賃レコード.f駅2}

and

RESULT

= w運賃レコード;

-- RESULTは、事後条件式の中だけで使える予約後で、返り値の値を示す。

LM 7.1 let式 (let be式)

LM 6 関数定義

let be式

構文: 式 =

let 式

|

let be 式

| . . . ;

let 式 = ‘let’,

ローカル定義

{ ‘,’,

ローカル定義

}, ‘in’,

式

;

let be 式 = ‘let’,

束縛

, [ ‘be’, ‘st’,

式

], ‘in’,

式

;

ローカル定義 =

値定義

| 関数定義;

値定義 =

パターン

_{, [ ‘:’,}

型

_{], ‘=’,}

式

_;

LM 7.1 let式 (let be式)

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

パターン

n

パターン

l

パターンはある特定の型の1つの値に一

致する。

n

パターン識別子

l

どんな型のどんな値にも一致する。

l

識別子の場合

n

_{識別子がその値に束縛される}

l

don't-care記号'-'の場合

n

束縛は起きない

n

他のパターンは中級以上で使用す

るので、説明しない

構文: パターン =

パターン識別子

|

一致値

|

集合列挙パターン

|

集合合併パターン

|

列列挙パターン

|

列連結パターン

|

写像列挙パターン

|

写像併合パターン

|

組パターン

|

レコードパターン

;

パターン識別子 =

識別子

| ‘-’

識別子 = (

文字

_{), { (}

_文字

_{| ‘'’ | ‘_’ } ;}

LM 8 パターン

パターン識別子の例

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記号'-'と一致させて、束縛が起きないようにし、

この後使わないようにしている。

束縛

構文: 束縛 =

集合束縛

|

型束縛

;

集合束縛 =

パターン

_{, ‘in set’,}

式

_;

型束縛 =

パターン

_{, ‘:’,}

型

_;

束縛リスト =

多重束縛

_{, { ‘,’,}

多重束縛

_{} ;}

多重束縛 =

多重集合束縛

|

多重型束縛

;

多重集合束縛 =

パターンリスト

_{, ‘in set’,}

式

_;

多重型束縛 =

パターンリスト

_{, ‘:’,}

型

_;

LM 9 束縛

n

束縛は、パターンと一致する値の範囲を指定する。

n

集合束縛では、値は集合から選ばれ、

n

型束縛では、値は型から選ばれるので、自然数(nat)型など無限の要素がある型は

実行できない。

束縛の例

集合束縛

{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

LM 4.2.1 集合型 演算子

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

運賃表

--運賃表クラスの定義がここで終わることを示す。

「運賃表集合に存在する」か判定する関数

集合内包式

集合式の構文

構文: 式 = . . .

|

集合内包

| . . . ;

式リスト =

式

_{, { ‘,’,}

式

_{} ;}

集合内包 = ‘{’,

式

_{, ‘|’,}

束縛リスト

_{, [ ‘&’,}

式

_{], ‘}’ ;}

多重集合束縛=

パターンリスト

_{, ‘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

運賃計算クラス

class

運賃計算

is subclass of

運賃表

--運賃計算クラスが運賃表クラスのサブクラスであることを示す。

instance variables

--インスタンス変数の定義。VDM++では、インスタンス変数のみが広域(グローバル)変数。

s運賃表集合 : 運賃表集合 := {};

--s運賃表集合は、他のクラスからはアクセスできないprivateな運賃表集合型のインスタンス変数で、

--初期値は空集合である。

operations

-- 構成子はクラスのインスタンスを生成する。

-- 引数なしの構成子は自動的に生成されるので、ここで定義する必要はない。

public

運賃計算 : 運賃表集合 ==> 運賃計算

--構成子の操作名と返り値の型名はクラス名と同じでなければならない。

運賃計算

(a運賃表集合) == s運賃表集合 := a運賃表集合;

--引数で受け取った内容を、インスタンス変数に代入(記号は":=")する。

LM 11 インスタンス変数

{

mk_

運賃表

`運賃レコード(

"東京"

,

"品川"

, 220),

mk_

運賃表

`運賃レコード(

"東京"

,

"新宿"

, 180),

mk_

運賃表

`運賃レコード(

"新宿"

,

"品川"

, 190)};

LM 13.4 代入文

「運賃を得る」操作(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

--操作の事後条件。操作の事後条件では、インスタンス変数を使用できる。

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

運賃計算

LM 7.5 1存在限量式

LM 13.10 return文

LM 13.1 let文

ここまでのまとめ

テストケース階層

✔

業務論理階層

テストケースの作成: 簡易回帰テスト

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]を返す。

簡易回帰テストの個々のテストケース

operations

public

t1 : () ==>

bool

--1番目の回帰テストケースの操作。うまく行ったか否かをbool型で返す。

t1() == (

-- '('から')'までが1つのブロック分で、複数の文を記述できる。

--今は、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

return

w運賃計算.運賃を得る(

"東京"

,

"新宿"

) = 180

);

...

end

Test

LM 13.3 ブロック文

LM 13.1 let文

ここまでのまとめ

✔

テストケース階層

✔

業務論理階層

組み合わせ(Combinatorial)テスト

class

UseFare0

values

--定数の定義

v運賃レコード集合 : 運賃表`運賃表集合 = {

-- 「運賃表`運賃表集合」は、運賃表クラスの運賃表集合を示す。

mk_

運賃表

`運賃レコード(

"東京"

,

"品川"

, 220),

mk_

運賃表

`運賃レコード(

"東京"

,

"新宿"

, 180),

mk_

運賃表

`運賃レコード(

"新宿"

,

"品川"

, 190)

};

instance variables

sTest : Test :=

new

Test();

組み合わせ(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通りの組み合わせが生成され、

LM 17 traces定義

簡単な演習

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

例外処理例

LM 13.11 例外処理文 (exit文)

LM 13.11 例外処理文 (trap文)

LM 4.2.4 組型 (演習には使わない)

LM 4.1.4 引用型

演習問題1

n

例外処理文を使って、Fare0モデルのエラー処理仕様を記述せよ

l

ヒント:

n

業務論理階層のクラス内の操作の事前条件を注釈とし、exit文

でエラーの場合に例外を発生させる文を追加する

l

Fare0モデルの場合、「運賃を得る」操作を修正すれば良い

l

Fare0.vdmppを修正

n

発生する例外の処理をtrap文で記述するクラスを記述する

l

Fare0モデルの場合、回帰テストケースでtrap文を使用して、

意図的に発生させたエラーの例外をキャッチして、trueを返す

テストケースを書けば良い

l

Fare0_testspec.vdmppを修正

演習問題2

n

演習問題1で修正したFare0モデルをテストするため、組み合

わせテストを修正せよ

l

ヒント:

まとめ

n

形式手法の導入で成功している導入方法を参考に、実際の

仕様の100分の1モデルを通して、実用的なVDM++仕様を作

成し検証するための基本を紹介した。

n

今回、実際の仕様記述と検証で使用することの多いVDM++

関連の主な機能で紹介できなかったこと:

l

写像型、列型、トークン型、合併型と選択型

l

インスタンス変数の不変条件

l

実用的な回帰テストライブラリ

n

より詳しい副読本は、以下を参考にしていただきたい。

l

SEC-FM1-B-1 対象を如何にモデル化するか? 形式記述サンプル付き (簡易製本配布)

参考: VDMのツール

ツール

開発者

仕様

インタープリタ

IDEベース環境

特徴

VDMTools

SCSK

独自(C++)

独自(Qt使用)

Java, C++生成。オブジェクト

数が多い場合、vdmjより速

い。クラス図生成。

vdmi

Nick Battle

Fujitsu

Services(英国)

独自(Java)

IDE無し

オブジェクト数が少ない場合

は、VDMToolsより速い。

Overture

Tools

Overture Project

(デンマーク、英国、

オランダ、ポルトガ

ル、日本)

VDMJのソース

を利用

Eclipse

Java生成。オブジェクト数が

少ない場合は、VDMToolsより

速い。クラス図生成?

Vienna Talk

小田朋宏

SRA

VDMJをプロ

セス間通信で

利用

Pharo

Smalltalk

VDM-SL仕様が対象。

Smalltalk生成。