「形式手法と仕様記述」の探求に向けて〜形式手法とは？〜
国立情報学研究所 石川 冬樹
f-ishikawa@nii.ac.jp
2012/5/11

石川 @ SQiP演習コースⅡ第1回

1

自己紹介
石川 冬樹
from 国立情報学研究所 http://www.nii.ac.jp/
http://research.nii.ac.jp/~f-ishikawa/

産業界向け形式手法入門・活用「トップエスイー」講師（SQiPよりも「大学」っぽい？単発セミナーも）http://topse.jp/ http://topse.or.jp/
実践ポータルサイト http://formal.mri.co.jp/
VDM++入門本

本職は研究のお仕事もWebサービス・クラウドも本職，法解釈なんかも
2012/5/11

石川 @ SQiP演習コースⅡ第1回

2この資料の内容「形式手法」「形式仕様」とは何なのかを知る
どういう問題に注目しているのか？
どういう考え方で解決を目指すのか？
具体的にはどういう手法・ツールがあるのか？
活用するために何を身につけ，検討するのか？

「形式仕様」と「仕様記述」？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

3

目次「形式手法」「形式仕様」とは何なのかを知る
どういう問題に注目しているのか？
どういう考え方で解決を目指すのか？
具体的にはどういう手法・ツールがあるのか？
活用するために何を身につけ，検討するのか？

「形式仕様」と「仕様記述」？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

4

仕様
重要： すべての基になる計画，設計・実装，テスト定義，チーム間や外注先との共有，派生・修正時の理解・分析，・・・

どう誤解の原因（曖昧さ等）をつぶしている？
どう誤り（不整合等）をつぶしている？
（どう前後の成果物とつないでいる？）

そうそう
それで！

2012/5/11

1 もしパケットがメッセージを含まなければ（パケット長がパケットヘッダのサイズ以下ならば），パケットは廃棄されなければならない．
２ 転送条件
2.1 ・・・

石川 @ SQiP演習コースⅡ第1回

5

問題（１）： 曖昧さ
記述においてその意味が一意に定まらない記法（日本語，図等）自体で一意に決まっていない
一意に定め用いる運用を徹底していない・できない
フラグ1がONになるまではフラグ2はOFF
フラグ1がONになった後に限り，必要なタイミングで， フラグ1がONとなると同時にフラグ2をONにフラグ2をONにして欲しい
参加者は研究会の開始前に参加するコースを選択する
参加者は研究会の開始前に出席簿に記入する
事務は研究会終了時に担当講師への謝金振込を行う
えーと振込タイミングは・・・
2012/5/11

石川 @ SQiP演習コースⅡ第1回

6

問題（２）： 誤り（不整合）「正しくない」振る舞いを定めてしまう「何が正しくて何が正しくないか」という基準を明確に洗い出し，明記，共有していない
その基準を満たしているかどうかを，一定程度の信頼ができる方法で分析，検証していない
ダブルブッキングが起きることはない
様々な種類の予約操作の一部において，
ダブルブッキング防止のチェックが抜けている
複数プロセスが特定のタイミングでそれぞれリクエストを実行しロックをかけるとデッドロックが発生してしまうことがある
2012/5/11

石川 @ SQiP演習コースⅡ第1回

7

補足： 開発の段階と不具合修正コスト
青字：
不具合が埋め
込まれる場所黒字：
不具合が発見
される場所
赤字：
不具合の除去におけるコストの増加率[P. H. Feilerら, System Architecture Virtual Integration: An Industrial Case Study, 2009]2012/5/11

石川 @ SQiP演習コースⅡ第1回

8

補足： 開発の段階と不具合修正コスト

１．
早くバグ
を見つける

２．
バグ検出の
コストを下げる[The Economic Impacts of Inadequate Infrastructure for Software Testing, NIST, 2002]
2012/5/11

石川 @ SQiP演習コースⅡ第1回

9補足： 開発の段階と不具合修正コスト

ピークコストを下げる

累計コストを下げる[DSF Webサイト内の紹介資料]
2012/5/11

石川 @ SQiP演習コースⅡ第1回

10

目次「形式手法」「形式仕様」とは何なのかを知る
どういう問題に注目しているのか？
どういう考え方で解決を目指すのか？
具体的にはどういう手法・ツールがあるのか？
活用するために何を身につけ，検討するのか？

「形式仕様」と「仕様記述」？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

11

形式手法とは？（定義）
数理論理学等に基づき品質の高い
ソフトウェアを効率よく開発するための科学的・系統的アプローチ
システムの注目する側面を正確に，曖昧さのない言語で表現する曖昧さや思い込みを開発プロセスの早期に排除し，
手戻りによるコストを防ぐシステムの満たす性質について科学的・系統的な分析・検証を行い，品質を高める
2012/5/11

石川 @ SQiP演習コースⅡ第1回

12

形式手法とは？（もっと軽く）
仕様・設計を「きちんと」書く過程により曖昧さを解消することになる
不正確さ，不整合も表面化するシステムに対する理解が深まる

厳密な文法・意味論を持つ言語を用い

数理論理学がベース

仕様や設計を「きちんと」書いた結果により内容・方法は様々
誤解なく情報を共有できる
科学的・系統的な分析・検証ができ，
特にツールに支援させることができる

開発早期における信頼性確保※ 分析・検証の仕組みは，プログラムに対して活用することも多い
2012/5/11

石川 @ SQiP演習コースⅡ第1回

13

形式手法とは？（プログラムと対比）プログラムを書くと厳密な文法・意味論を持つ言語を用い

対象が厳密，明確に，
数理論理学がベース書き出される
型チェック，テストなどの内容・方法は様々
分析・検証を行える

上流の中間成果物（仕様・設計）でも！
ただしプログラムのように「一通り動かす」ことが目的ではないため，記述，分析・検証の目的に応じ，システム内で扱う対象（範囲・観点）を絞る
用いる言語，手法・ツールを選ぶ
2012/5/11

石川 @ SQiP演習コースⅡ第1回

14

ポイント： 「モデル」「モデル」： 計算や予測を助けるために用いられる，システムやプロセスの単純化された記述（しばしば数学的なもの）（Oxford英英辞典の石川訳）

注目する側面に特化し，抽象化・単純化（言い換えると，不要な実現詳細を捨象）

ツールが効率的に，系統的に検査を行える人間も重要な本質に集中して問題の分析を行える
2012/5/11

石川 @ SQiP演習コースⅡ第1回

15

形式手法への（今さらの）注目
日本語での書籍が出始め，セミナーも多数
SPIN，VDM，Alloy，B，・・・

導入促進のための活動が行われている
導入ガイダンス（2011年5月）
経産省（MRI，NII）
http://formal.mri.co.jp/
適用手順・イディオム（2011年7月）
Dependable Software Forum （DSF）
http://www.nttdata.co.jp/dsf/
・・・（技術の基礎は数十年前から）
2012/5/11

石川 @ SQiP演習コースⅡ第1回

16

目次「形式手法」「形式仕様」とは何なのかを知る
どういう問題に注目しているのか？
どういう考え方で解決を目指すのか？
具体的にはどういう手法・ツールがあるのか？
活用するために何を身につけ，検討するのか？

「形式仕様」と「仕様記述」？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

17

実際の手法・ツール
先の広い定義に対し，実際には様々な目的に応じて様々なアプローチがある
記述言語： 特定の側面に関する記述に特化していることが多い
データ構造？状態遷移？並行動作も書く？

検証方法： 様々で，記述言語とも強く関連する証明（理屈で正しさを示す）？
モデル検査（実行パスを網羅し正しさを示す）？
テスト（特定の状況を調べてみる）？

プロセス： 想定する利用工程やその入出力
2012/5/11

石川 @ SQiP演習コースⅡ第1回

18

大ざっぱな分類
形式仕様記述「仕様」として，システムの状態（データ構造）や，操作やイベントによるその変化を一通り記述する
記述および分析・検証の方針が，手法とツールによって様々である

代表的な手法： VDM，B，Event-B，Alloy

モデル検査
特に分散・並行システムなど，複雑な状態遷移に絞って記述を行い，網羅的な検証を自動的に行う（これが基本的な共通の考え方で，あとはツールの特性が異なるものがいくつか）

代表的なツール： SPIN，SMV，LTSA，UPPAAL
2012/5/11

石川 @ SQiP演習コースⅡ第1回

19

手法・ツールの例（１）： VDM（演習コースⅡでの取り組み候補の一つ）

VDM： 形式仕様（全体の記述）
プログラミングに比較的近い考え方で取り組め，普通のプログラマにとっつきやすい
動かしてみる・テストする
よくわからなければ最初の一歩によい
特に分析・検証については，「もっとすごいことができて欲しい」と思うかも
それでも「いいものが書ける」「効果が得られる」「活用できる」ためには，悩むこと，議論することがたくさん
2012/5/11

石川 @ SQiP演習コースⅡ第1回

20

手法・ツールの例（２）： SPIN
（演習コースⅡでの取り組み候補の一つ）

SPIN： モデル検査（状態遷移の検証）
並行・分散システムに関するよい勉強になる
マルチスレッド，マルチコア，クライアント・
サーバ，二重化などを含むシステム
デッドロック，安全性，活性，公平性，・・・
排他制御や通信制御などにピンポイントで注目し，実機では再現できないような，タイミングや障害に起因する特定のバグを見つけ出せる「反例」が出るので，原因追及も行いやすい
逆に，それだけ（強力な検証に特化）
2012/5/11

石川 @ SQiP演習コースⅡ第1回

21

手法・ツールの例（３）： Alloy（演習コースⅡでの取り組み候補の一つ）

Alloy： 形式仕様（全体の記述）
モデル検査ツールの良さを採り入れた，強力だが比較的とっつきやすい分析・検証ツールがある
網羅的に調べてみる検証なので， 「数学的証明」
を行うような検証よりは，とっつきやすい
一方，記述方式に多少クセがあるかも
実装（How）から離れた記述のいい特訓にはなる
制約などの漏れを見つけやすくする，「モデル発見」のツールが面白いかもしれないとにかくいっぱい例を自動生成してみる
2012/5/11

石川 @ SQiP演習コースⅡ第1回

22

VDM： 位置づけ（再）（演習コースⅡでの取り組み候補の一つ）

VDM： 形式仕様（全体の記述）
プログラミングに比較的近い考え方で取り組め，普通のプログラマにとっつきやすい
動かしてみる・テストする
よくわからなければ最初の一歩によい
特に分析・検証については，「もっとすごいことができて欲しい」と思うかも
それでも「いいものが書ける」「効果が得られる」「活用できる」ためには，悩むこと，議論することがたくさん
2012/5/11

石川 @ SQiP演習コースⅡ第1回

23

VDM： 典型的な例題
イベント登録管理システム
ユーザ，部屋，イベントの情報を管理「部屋R1の定員は30名である」「イベントE1は部屋R1で5/11の10-17時に開催」
予約やそのキャンセルの受付「ユーザ1が，イベントpに対して2名予約登録」→ 「座席A-35/A-36，予約番号1035Aを割り当て」「20100035Aの予約をキャンセル」「イベントqに対し，ユーザ1〜9999から5名を抽選で選び予約登録」

2012/5/11

石川 @ SQiP演習コースⅡ第1回

24

VDM： 検討する「正しさ」の基準（曖昧さの問題に加えて）システムの状態が常に満たすべき条件
例： 同じ時間に行われる複数イベントに対し，同じユーザが予約を行っていることはない

操作実行にあたり守るべき前提条件
例： キャンセル操作は，開催日が次の日以降のイベントに対してのみ実行可能である操作に期待される効果を定める条件
例： 抽選操作の実行結果においては，
実行前に対象イベントに対し，予約を行っていなかったユーザが選択されている
2012/5/11

石川 @ SQiP演習コースⅡ第1回

25

VDM： システム状態のモデル
予約情報

イベント情報

予約番号
ユーザ
イベント
座席

10
U1
VDM2012{1, 2, 3}

予約番号
ユーザ
イベント
座席

21
U4
SPIN2011{5, 7}

・・・

部屋情報

ユーザ情報

・・・

・・・

CPU・メモリ上でどう「うまく」動かすか（How）には触れず，システムが何をするか（What）
を抽象的（だが厳密に）定義，記述

・・・
予約番号
ユーザ
イベント
座席

2012/5/11

32
U2
VDM2012{11, 12}

登録満たすべき正しさの基準も明確に定義，記述

石川 @ SQiP演習コースⅡ第1回

26

VDM： 記述イメージ（１）class EventManager
instance variables
users : set of User := {};rooms : set of Room := {};オブジェクト指向型の記述も可能（VDM++言語）「順序を付けず複数のデータを保持（set）」という抽象データ構造（検索効率等気にしない）

events : set of Event := {};inv (forall ev1, ev2 in set events &ev1 <> ev2 =>
ev1.room <> ev2.room or ev1.date <> ev2.date);

reservations : set of Reservation := {};inv …
2つのイベントが同じ日時，
operations
同じ時間に行われることが…
ないという条件の記述
2012/5/11

石川 @ SQiP演習コースⅡ第1回

27

VDM： 記述イメージ（２）public searchUsersByEvent : Event ==> set of User
searchUsersByEvent(event) ==return { res.user | res in set reservations &res.event = event }条件を満たすユーザを
pre event in set events;
すべて抜き出すという，
この操作が正しく実行可能な記述実行できる前提条件（実行効率等気にしない）
public sortEventsByUser : set of Event ==> seq of Event
sortEventsByUser(event) == is not yet specified
post forall i, j in set inds RESULT &i < j => RESULT(i).date < RESULT(j).dateand …;
戻り値のリストにおいては，イベントが日付が早い順に並んでいることなど明記（期待する実行結果だけを記述）
2012/5/11

石川 @ SQiP演習コースⅡ第1回

28

VDM： ツールイメージ

インタプリタから
テストメソッド呼び出し

カバレッジ出力

事前条件
チェックエラー
2012/5/11

石川 @ SQiP演習コースⅡ第1回

29

SPIN： 位置づけ（再）（演習コースⅡでの取り組み候補の一つ）

SPIN： モデル検査（状態遷移の検証）
並行・分散システムに関するよい勉強になる
マルチスレッド，マルチコア，クライアント・
サーバ，二重化などを含むシステム
デッドロック，安全性，活性，公平性，・・・
排他制御や通信制御などにピンポイントで注目し，実機では再現できないような，タイミングや障害に起因する特定のバグを見つけ出せる「反例」が出るので，原因追及も行いやすい
逆に，それだけ（強力な検証に特化）
2012/5/11

石川 @ SQiP演習コースⅡ第1回

30

SPIN： 典型的な例題
食事する哲学者
並行プログラムの比喩

左右どちらかのフォークをとった後，もう片方をとり，食事をしてフォークを戻す（会話はしない）
ようなプログラムを設計

うまく行動を定めないと，
特定の振る舞いの順序でデッドロックやライブロック
例： 全員が左のフォークを持ち右が空くのを待ち続ける
2012/5/11

石川 @ SQiP演習コースⅡ第1回

31

SPIN： 検討する「正しさ」の基準
デッドロックフリー
誰も何もできなくなる状況に到達しない

進行性（活性）
食べる以外の行動（様子見・断念してフォークを置く等）を全員が繰り返すだけの状況に陥らない

公平性ある哲学者が（ある定義で）「ずっと」食べることができないような状況に陥らない

2012/5/11

石川 @ SQiP演習コースⅡ第1回

32

SPIN： 状態遷移のモデル「右手側からフォークをとる（とったら戻さない）」ルール・3人版
システム全体p0 p1

哲学者p0
fork0が空いていたら（空くまで待つ） 右手： 空き
右手でとる
左手： 空き食べてフォークを戻す

右手： fork0
右手： fork0
左手： 空き左手： fork2
fork2が空いていたら（空くまで待つ）
左手でとる

2012/5/11

p2

システム全体では，3名の振る舞いが「からみあって」複雑な状態遷移になる

石川 @ SQiP演習コースⅡ第1回

33

SPIN： 状態遷移のモデル（全体）p2右手

fork0： 空き
fork1： 空きfork2： 空き
p0右手

・・・

p1右手

・・・
P0食

P0食

fork0： p0（右手）p0左手
fork0： p0（右手）fork1： p1（右手）fork0： p0（右手）fork1： 空きfork2： p0（左手）fork1： 空きfork2： p0（左手） p1右手fork2： 空き
p2左手・・・
p2右手 fork0： p0（右手）fork1： 空き
p1右手fork2： p2（右手）p1右手

fork0： p0（右手）fork1： p1（右手）fork2： 空き

p0左手
p2右手

fork0： p0（右手）fork1： p1（右手）fork2： p2（右手）デッドロック2012/5/11

石川 @ SQiP演習コースⅡ第1回

34

SPIN： 記述例
mtype = {p0, p1, p2, none};
列挙型
mtype fork[3] = none;
原子的に，フォークがactive proctype P0(){
空いているなら確保
do:: atomic{fork[0] == none -> fork[0] = p0};
atomic{fork[2] == none -> fork[2] = p0};
skip;
「食べる」ことは今回のfork[2] = none;
モデル化で本質では
fork[0] = none;
od
ないので捨象}
合成はツール側で...
[ ] (fork[2]==p2 -> <> fork[1]==p2)

正しさの基準もP2が右手のフォークをとったときはいつでも，
その後いつか左手のフォークをとる
2012/5/11

石川 @ SQiP演習コースⅡ第1回

35

SPIN： ツールイメージ

そのパスのトレース

デッドロックに至る
最短のパスを検索（古いGUIです）
通信がある場合それも図示
2012/5/11

石川 @ SQiP演習コースⅡ第1回

36

SPIN： 別の記述例（通信含む）#define SIZE 4
byte msg[SIZE];
chan s2r = [2] of {byte};

バッファ長さ2，byte型の通信チャンネル
proctype Sender() {byte i;do:: i == SIZE -> break;:: else -> s2r ! msg[i];i++;od 配列内のメッセージを}順次送信

2012/5/11

proctype Receiver() {byte j;byte rmsg;
do:: j == SIZE -> break;:: else -> s2r ? rmsg;
assert (rmsg == msg[j]);j++;odメッセージを受信，}順番通りか検証

proctype Lost() {byte drop;do:: s2r ? drop;od}

石川 @ SQiP演習コースⅡ第1回通信の失敗を表現（メッ
セージを受信してしまう）
37

Alloy： 位置づけ（再）（演習コースⅡでの取り組み候補の一つ）

Alloy： 形式仕様（全体の記述）
モデル検査ツールの良さを採り入れた，強力だが比較的とっつきやすい分析・検証ツールがある
網羅的に調べてみる検証なので， 「数学的証明」
を行うような検証よりは，とっつきやすい
一方，記述方式に多少クセがあるかも
実装（How）から離れた記述のいい特訓にはなる
制約などの漏れを見つけやすくする，「モデル発見」のツールが面白いかもしれないとにかくいっぱい例を自動生成してみる
2012/5/11

石川 @ SQiP演習コースⅡ第1回

38

Alloy： 一つの例題
メールアドレス帳の仕様定義
グループには1個以上の要素が含まれる
エイリアスは1個だけの要素を含む
Group1
Alias4Address3

Address5[抽象によるソフトウェア設計−Alloyではじめる形式手法−] より
2012/5/11

石川 @ SQiP演習コースⅡ第1回

39

Alloy： 記述イメージ（１）型やクラスのようなもの

abstract sig Target {}（signature）を定義
sig Addr extends Target {}abstract sig Name extends Target {}AliasかGroupからはsig Alias, Group extends Name {}少なくとも1つのTargetを指す
sig Book {names: set Name,{ (Group1, Alias4),
addr: names -> some Target }(Alias4, Address5), …}{
all a: Alias | lone a.addr
Aliasは高々1つのTargetを指す}[抽象によるソフトウェア設計－Alloyではじめる形式手法－] より
2012/5/11

石川 @ SQiP演習コースⅡ第1回

40

Alloy： ツールイメージ（１）
この時点でツールを使ってみる（Alloy Analyzer）
pred show (b: Book) {#b.addr > 1}
run show for 3 but 1 Book

リンクを2個以上含むような構造例を表示してみる
諸々を最大3個生成して（アドレス帳だけは1個）
構造例を探すGroup1
Address1

Group1

Address2

Address1

適当に名前が付いていろいろ生成される
2012/5/11

石川 @ SQiP演習コースⅡ第1回

41

Alloy： 記述イメージ（１・修正）
abstract sig Target {}sig Addr extends Target {}abstract sig Name extends Target {}sig Alias, Group extends Name {}sig Book {names: set Name,
addr: names -> some Target }どの要素からも，リンクを{
all a: Alias | lone a.addr
任意の回数たどって，
no n: Name | n in n.^(addr)
自分に戻ってくることはない}[抽象によるソフトウェア設計－Alloyではじめる形式手法－] より
2012/5/11

石川 @ SQiP演習コースⅡ第1回

42

Alloy： 記述イメージ（２）abstract sig Target {}sig Addr extends Target {}abstract sig Name extends Target {}sig Alias, Group extends Name {}sig Book {names: set Name,
addr: names -> some Target }{リンクの追加と削除に関する
all a: Alias | lone a.addr
操作定義を追加
no n: Name | n in n.^(addr)}
pred add (b, b’: Book, n: Name, t: Target){b’addr = b.addr + n -> t}pred del (b, b': Book, n: Name, a: Addr){b'.addr = b.addr - n-> a}[抽象によるソフトウェア設計－Alloyではじめる形式手法－] より
2012/5/11

石川 @ SQiP演習コースⅡ第1回

43

Alloy： ツールイメージ（２）assert delUndoesAdd{
all b, b', b'': Book, n: Name, a: Addr |add [b, b', n, a] and del [b', b'', n, a]
implies b.addr = b''.addr}
check delUndoesAdd for 3

どんなアドレス帳，名前，
アドレスでも，同じリンクを追加し，そのリンクを削除すると，最初に戻る？

諸々を最大3個生成して網羅的に調べてみる
Group1
Address1

Address2

Group1
Address1

add Group1->Address2
2012/5/11

Address2

Group1
Address1

del Group1->Address2

石川 @ SQiP演習コースⅡ第1回

44

補足： プログラムでの活用プログラムにて様々な条件を記述
例： JML（Java Modeling Language）（ユニットテストへのアサーション埋め込みツール
や，潜在エラーの警告ツール）

プログラムに対するモデル検査（ソフトウェアモデル検査）
例： Java PathFinder

抽象モデルよりも，検証内容が詳細になる
ポインタ，非null条件，配列インデックス，・・・
コードやその実行環境が複雑なので，検証能力に限界が生じたり，工夫が必要になったりする
2012/5/11

石川 @ SQiP演習コースⅡ第1回

45

目次「形式手法」「形式仕様」とは何なのかを知る
どういう問題に注目しているのか？
どういう考え方で解決を目指すのか？
具体的にはどういう手法・ツールがあるのか？
活用するために何を身につけ，検討するのか？

「形式仕様」と「仕様記述」？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

46

形式手法とは？（再）仕様・設計を「きちんと」書く過程により曖昧さを解消することになる
不正確さ，不整合も表面化するシステムに対する理解が深まる

厳密な文法・意味論を持つ言語を用い

数理論理学がベース

仕様や設計を「きちんと」書いた結果により内容・方法は様々
誤解なく情報を共有できる
科学的・系統的な分析・検証ができ，
特にツールに支援させることができる

開発早期における信頼性確保※ 分析・検証の仕組みは，プログラムに対して活用することも多い
2012/5/11

石川 @ SQiP演習コースⅡ第1回

47

学ぶこと： 準備
基礎知識： 数理論理学の基礎の基礎
集合論：
メモリなどを想定した操作の仕組みや効率に触れずに，状態やその変化を表現する道具
命題論理・述語論理：
Yes/No と明確に判断できる言い回しをする道具
プログラムのif文などの条件式より少し強力に（＋ 個々の手法・ツールで必要なもの）
あとはSPINの場合の「時相論理」くらい

2012/5/11

石川 @ SQiP演習コースⅡ第1回

48

学ぶこと
形式手法の考え方
様々な手法・ツールの知識（短期で学ぼうとしてもたぶん何も身につかない）

1個の手法・ツールの技術を学ぶことを通し，形式手法の考え方と十分向き合い，体験し，それに従って，定義や記述，分析・検証の良し悪しの議論
や，進め方の検討を行えるようになる
特定手法・ツールを使えることは二の次？
自分たち自身が向き合わなければならない難しさを実感するところまで踏み込む
形式手法の考え方やその手法・ツールの利点と欠点・限界を，実感をもって議論できるようになる
2012/5/11

石川 @ SQiP演習コースⅡ第1回

49

検討・議論すること自分たちが抱える問題点との関連性・マッチン
グを考え抜く
考え方の必要性，活用方法（マッチするなら）特定の手法・ツールの必要性，
活用方法

自分たちが抱える問題点と，考え方や手法・ツールとのギャップを考え抜く
あくまで解法の基（種）
何がまだ足りないのか？
となる一般論
どれだけ効果的なのか？
どうすれば「今の現場」にはまるのか？
「演習」だとしても，これらが・・・（山ほど）ないと，ほぼ意味がない！
2012/5/11

石川 @ SQiP演習コースⅡ第1回

50

取り組みの例（１）
日本語による仕様記述の考え方（清水さんのものなど）とは，どう得意なこと・効果が違い，どう補完するのか？
テストファーストといった考え方で仕様を向上する
こととは，どう得意なこと・効果が違い，どう補完するのか？
WebアプリのようにHow（実装フレームワーク）が早い段階から決まっている場合に，どこまでどう
Howを意識した記述を上流で行うべきか？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

51

取り組みの例（２）
去年すごくはまった，うちのあの案件で，もしも形式仕様を使っていたらどうなっていただろうか？
現状用いているExcelベースのWebアプリ設計書に対し，必要なところだけ厳密な言語を決めて，テスト
自動生成・実行を可能にできるか？
この業界でいつも使っているフォーマットからの言語変換により，皆にできる限り意識させずに，形式
手法のツールを使うようにできるか？
Howのない形式仕様から，どうHowを入れ込んでプ
ログラムを効率よく導けばよいか？
2012/5/11

石川 @ SQiP演習コースⅡ第1回

52

目次「形式手法」「形式仕様」とは何なのかを知る
どういう問題に注目しているのか？
どういう考え方で解決を目指すのか？
具体的にはどういう手法・ツールがあるのか？
活用するために何を身につけ，検討するのか？

「形式仕様」と「仕様記述」？

2012/5/11

石川 @ SQiP演習コースⅡ第1回

53

個人的な思想「形式手法」そのものは，最終的に現場で使わなくてもよいです「手段」を「目的」に変えないでください
特に「強力な検証」の方は，必要なとき，必要なポイントで，必要な人が使えればよいです
もちろん，本当にニーズに合致するならぜひ使ってください

それより，今日聞いたことを，明日（今日）活きる意識，原則（注意点）にしましょう！
要求仕様や設計の内容の決め方，日本語としての表
現の仕方，レビューの仕方，・・・
2012/5/11

石川 @ SQiP演習コースⅡ第1回

54