Document

pre formalから
exploratory formalにおける
ツール支援
小田朋宏
Software Research Associates, Inc.
2015/3/24 @福岡
Agenda
● pre formalとexploratory formal
o
o
●
●
●
●
●
どのような工程があるか
problem framing問題
VDMPadによる支援
Lively Walk-Throughによる支援
Cloudly Walk-Throughによる支援
課題
まとめ
pre formal
and
exploratory formal
informalからimplementationまで
informal requirements
なんとなくの話
pre formal specification
核心部分を見極める
どこをformalに書くか
exploratory formal spec
試行錯誤
どう書けばうまく行くか
rigorous formal spec
仕様の正しさに確信を持つ
仕様を系統的に扱う
implementation
確信のある仕様を有効に使う
pre formalとexploratory formal
pre formal
● 形式化するスコープを決める
● 形式化する語彙を決める
● problem framing
o 例：チェッカーボード問題
exploratory formal
● ドメインによる適切な抽象を探る
● 言語による適切な抽象を探る
● 妥当性を確認しながら
必要に応じてpre formalに立ち返る
problem framing
チェッカーボード問題
(Fischer, AVI2006から引用)
チェス盤がある。ドミノで2マスずつ埋めたい。
普通のチェス盤なら埋まる。
図のように対角線にある2つだけが欠けている場合には？
とある解法
pythonで全空間探索するプログラムを書いて
制約を満たすドミノの配置が存在しないことを
確認した。
コネクタ問題
(Fischer, AVI2006をアレンジ)
32本のケーブルと32個のコネクタがある
1本のケーブルに1個のコネクタを半田付けする
つもりが、
半田付けを失敗して2個のコネクタをダメにし
てしまいました
32本全てのケーブルと残る30個のコネクタで
部品を残さず半田付けできるでしょうか？
チェッカーボード問題 revisited
(Fischer, AVI2006から引用)
赤いマスが32個、黒いマスが30個あります。赤と黒のマス
を1つずつ隠すドミノで全部のマスを隠せますか？
ソフトウェア開発ならば
● 開発者が顧客に
解法としてのシステムを説明/提案する
o
o
o
妥当性の確認
顧客にとってどちらが理解しやすいか？
「プログラムで全空間探索しました」
vs
「赤いマスと黒いマスの数が合いません」
適切なproblem framingが必要
problem framing は formal methods
の範囲内？
● YES
o
問題の形式化に不可欠な過程
o
数学/計算理論でよく見かける
対角線論法
補題
NP完全問題
●
ある問題を既知の問題に帰着させる
全空間探索とコネクタ問題の分岐点
不適切な抽象
この絵をどれだけ見つめても、
コネクタ問題との繋がりは見えない
problem framingへのツール支援
● ツールによる自動化は困難
● 自動化はできなくても支援は可能？
o
解法のカタログ化
対角線論法、εδ論法、パターン言語、定石集
o
語彙の整理
チェッカーボードを8x8の盤に抽象したらダメ
o
発見的知識獲得
「隣接するマスのペア」が赤マスと黒マスをで
あることに気付く
abstraction of the language
abstraction of the domain
言語による抽象とドメインによる抽象
● 言語による抽象
o
o
ある概念をその言語のどの言語要素で表現するか
その言語を使う技術者に共有される
● ドメインによる抽象
o
o
o
どの粒度の概念を定義するか
ある概念に関連するルールや概念
顧客を含む開発チーム全体で共有される
ドメイン専門家からチーム全体に伝えられる
言語による抽象
● どの概念をどの言語要素で表現するか
o
o
o
o
o
function : state * args -> state
vs
operation : args ==> ()
型の不変条件
vs
状態の不変条件
vs
関数/操作の事前/事後条件
set vs map vs seq
内包表現 vs for文
などなど
ドメインによる抽象
● どの粒度の概念を定義するか
o
o
ドミノ
●
縦配置のドミノ
●
横配置のドミノ
チェス盤
マス
●
黒いマス
●
赤いマス
行、列
● ある概念に関連するルールや概念
o
o
ドミノを敷き詰める、とは？
マスが隣接している、とは？
tools
pre formalとexploratory formal
pre formal
● 形式化するスコープを決める
● 形式化する語彙を決める
● problem framing
o 例：チェッカーボード問題
exploratory formal
● 言語による適切な抽象を探る
● ドメインによる適切な抽象を探る
● 妥当性を確認しながら
必要に応じてpre formalに立ち返る
大森先生の
辞書ツール
佐原さんの
イディオム・定石
VDMPad
Lively / Cloudly
VDMPad
Lively / Cloudly
Walk-Through
exploratory formal
● 「適切に」表現できる記述の切り口を探す
o
o
1つの問題の表現は複数ありうる
言語による抽象
● 仕様記述者がドメイン知識を獲得する
o
o
ドメイン専門家からの意見を獲得する
ドメインによる抽象
exploratory formalへのツール支援
● 言語による抽象
o
o
●
media for reflection:
自分で考えるためのメディア
VDMPad
ドメインによる抽象
o
o
o
media for communication:
他者から意見を得るためのメディア
Lively Walk-Through (UIデザイナとの対話)
Cloudly Walk-Through (ドメイン専門家との対話)
VDMPad
VDMPad
● 言語による抽象を支援する
● アニメーションを軸にした試行錯誤
o
o
o
Specを素早く書き下ろす
いろいろな状態を作ってみて、
ビジュアル表現で俯瞰する
Workspace上で表現式を書いてみる
ザッピングTVリモコン
● 特に見たい番組がない時、いつものチャン
ネルを巡回して面白そうな番組がやってな
いか探したい。（ザッピング）
o
o
ザッピング用のリストにチャンネルを追加したり削
除したりしたい。
ザッピング用のリストのチャンネルで巡回したい。
型と状態
types
channel = nat
inv channel == channel >= 1 and channel <= 12;
state memory of
current : channel
zapList : seq of channel
zapIndex : [nat1]
inv
mk_memory(current, zapList, zapIndex) ==
zapIndex = nil or zapIndex <= len zapList
普通のリモコンとしての機能
operations
num : channel ==> channel
num(x) == (zapIndex := nil; current := x; return
current);
inc : () ==> channel
inc() == return num((current mod 12) + 1);
dec : () ==> channel
dec() == return num(((current - 2) mod 12) + 1);
get : () ==> channel
get() == return current;
ザッピング関係
operations
toggleZap : () ==> channel
nextZap : () ==> channel
prevZap : () ==> channel
addZap : () ==> ()
delZap : () ==> ()
-- ユーザは見たい番組がある時とない時で行動が違う
-- 通常モードとザッピングモードを分離して
-- モード切り替えの操作 toggleZapと
-- ザップの順送り nextZapと逆送りprevZapと
-- 今のチャンネルをリストに追加 addZapと削除delZap
VDMPadで探究的に仕様を書く
Lively Walk-Through
Lively Walk-Through
● VDM仕様をUIデザイナに説明する
o
media for communication
● UIプロトタイプ作りを軸にした対話
o
UIデザイナはユーザの認知のドメイン専門家
o
UIデザイナがVDM仕様を理解することで
VDM仕様にUIデザイナのドメイン知識を
反映させることができる
ザッピング関係
operations
toggleZap : () ==> channel
nextZap : () ==> channel
prevZap : () ==> channel
addZap : () ==> ()
delZap : () ==> ()
-- ユーザは見たい番組がある時とない時で行動が違う
-- 通常モードとザッピングモードを分離して
-- モード切り替えの操作 toggleZapと
-- ザップの順送り nextZapと逆送りprevZapと
-- 今のチャンネルをリストに追加 addZapと削除delZap
VDM仕様を使ったUIプロトタイプ
UIデザイナの主張
● 安易にモードを作るな
o
o
ユーザにモードをどう把握させる？
ユーザがメンタルモデルを構築しにくい
● ユーザはチャンネルを巡回したいのであっ
て、順送りnextZapや逆送りprevZapは必要
ない
● チャンネルの順送りinc()や逆送りdec()に加
えて zap()があればいい
見直したzap機能
zap : () ==> channel
zap() == (
if zapList = [] then return current;
if zapIndex = nil
then zapIndex := 1
else zapIndex := zapIndex mod len zapList + 1;
current := zapList(zapIndex);
return current);
-- zapボタンを押せば、zapListに登録された順に
-- チャンネルを何周でも巡回する。
新しい仕様を使ったUIプロトタイプ
Cloudly Walk-Through
Cloudly Walk-Through
● ドメインによる抽象を支援する
o
media for communication
● ポンチ絵とアニメーションを軸にした対話
o
o
VDMの文法を知らない人のためのビジュアル表現
ポンチ絵による文脈の表現
Cloudly Walk-Throughによる
ポンチ絵
3つのツールのまとめ
● VDMPad
o
o
適切な言語抽象を探究
[仕様記述者による] 適切なドメイン抽象を探究
● Lively Walk-Through
o
[UIデザイナによる] 適切なドメイン抽象を探究
● Cloudly Walk-Through
o
[ドメイン専門家による] 適切なドメイン抽象を探究
これらの探究を通じてproblem framingの機会を得る
missing link
課題
鶏と卵
● 正しい抽象を得るためには
適切なproblem framingが必要
● 正しいproblem framingを得るには
適切な抽象が必要
解決するためには
● トンカチで叩くのではなく、ネジを回せ
o
形式手法の常道
● 異なる種類の専門家の知恵を得る
o
コミュニケーションメディアとしてのツール
● 経験の蓄積 → イディオム・定石
o
information retrieval / recommender systems
code clone
clustering, cataloging, discourse
wrap up
まとめ
● pre formal
o
o
形式化のスコープ、語彙: 大森先生のツール
problem framing: 佐原さんのイディオム・定石
● exploratory formal
o
o
言語による抽象：VDMPad
ドメインによる抽象：Walk-Through series
multidisciplinary communication
今後の課題
● 経験を蓄積し、適用するためのツール
o
o
o
経験をどうencodingするか
経験をどうretrieveするか
経験をどうdiscourseするか

Download Report