ライブ UI プロトタイピングに向けたマルチ言語環境
SOMETHINGit

小田朋宏(株)SRA中小路久美代(株)SRA山本恭裕

東京工業大学1

13年7月9日火曜日

UI design
Lightweight Formal Method

2
13年7月9日火曜日

動機• 軽量形式手法をより多くの人が手軽に使える環境を作りたいo

例えば、UIデザイナ

3
13年7月9日火曜日

軽量形式手法とUIデザイン
それぞれのプロトタイピングの特徴
実行可能仕様• 実行可能性• 厳密性

UIスケッチ• 具体性• ニュアンス
4
13年7月9日火曜日

軽量形式手法＋UIプロトタイピング
UIデザイナ

形式手法技術者

実行可能なUIプロトタイプ
デザインデシジョンの合意
5
13年7月9日火曜日

めざすところ• 「機能モデル的に実現可能なUIデザイン」
かつ、「適切なUIを構築可能な機能モデル」
ができるようなプロトタイプ環境を作りたい

6
13年7月9日火曜日

本研究開発のアプローチ
UIをデザインすることと機能をモデリングすることを共同デザインとして捉えるUIデザイナと形式手法技術者の間の「対話」のデザイン

プロトタイピング環境構築に必要なライブラリの実装
UIプロトタイピング環境の構築
7
13年7月9日火曜日

LIVE

8
13年7月9日火曜日

合意形成のためのプロトタイピング• プロトタイプの定義とビュー双方について
o

仮説的状況を実現して試行できることo

何が起こっているのか理解できること

o

手に取って指し示して議論できること

そこでo プロトタイプを定義する記述環境
o プロトタイプを使う実行環境を同一にする＝ ライブプロトタイピング環境
9

13年7月9日火曜日

SOMETHINGit

10
13年7月9日火曜日

SOMETHINGit• Smalltalk (Squeak/Pharo) 上のライブラリo外部インタプリタを呼び出す§§

VDM-SL (VDMJ)
Haskell (GHCi)• ライブプロトタイピングを指向o

VDM-SLでのSmalltalk流のライブなプロトタイピングを可能にする
11

13年7月9日火曜日

SOMETHINGitによる
Smalltalk流プログラミング環境の実現• 情報隠蔽を破るバックドア• 実行時改変と継続実行• 自由度の高いFFI

12
13年7月9日火曜日

Backdoors

13
13年7月9日火曜日

情報隠蔽を破るバックドア
VDM-SLモジュールのstate内の変数はprivate• 外部から値を読んだり書き込むためにはoperationを通す必要がある• そこでstate内の全変数に一括して読み書きするpublicなアクセサを自動生成する
oo

settergetter14
13年7月9日火曜日

安全なバックドア
VDM-SL仕様中ではバックドアを利用できない
1. バックドア無しの仕様をVDMJにロードする
2. コンパイルエラーが発生しなければa.

バックドアを自動生成しb.

バックドア付きの仕様を再ロードする

15
13年7月9日火曜日

例：state変数の値を直接操作するモジュールリスト

変数リスト

値

モジュールの仕様記述

16
13年7月9日火曜日

count * 10を計算する

VDMの式

17
13年7月9日火曜日

count * 10 の答えは140

評価結果

1813年7月9日火曜日

140を

19
13年7月9日火曜日

140を変数countの値に設定する

20
13年7月9日火曜日

変数countの値が140になる

21
13年7月9日火曜日

開発環境を「保存して終了」する

22
13年7月9日火曜日

一旦、開発環境を終了した後で

23
13年7月9日火曜日

もう一度開発環境を開くと終了前の状態が回復する

値がリセット
されていない

24
13年7月9日火曜日

Liveness

25
13年7月9日火曜日

ライブプログラミング
実行中のプログラムのソースコードを変更したら即座にその実行に反映される
プログラミング= 脱 Edit-Compile-Run サイクル

26
13年7月9日火曜日

例：プロトタイプ実行中の仕様変更

27
13年7月9日火曜日

state変数としてgoal : intを追加

変数goalを追加
初期化を追加

28
13年7月9日火曜日

変数goalを追加しても元の変数の値は維持されている

リセット
変数 goal がされていない

追加されている29
13年7月9日火曜日

変数goalの値はinitの定義通り0

初期化
されている

30
13年7月9日火曜日

変数goalを削除しても変数countの値は維持される

リセット
されていない

31
13年7月9日火曜日

実行時改変と継続実行のしくみ
1. バックドアを使って全モジュールのstateを読み出す
2. 変更後の仕様をロードする
3. 変更後の仕様のバックドアを生成する
4. バックドア付きの仕様をロードする
5. バックドアを使って、全モジュールのstateに書き込む
32
13年7月9日火曜日

Expression-based
Foreign Function Interface

33
13年7月9日火曜日

自由度の高い言語間インターフェイス
通常の言語間インターフェイス(FFI)• 関数名、引数の数と型、返り値の型を前もって公開する

SOMETHINGitの表現式ベースのFFI• 外部DSLとして任意の表現式を埋め込むことが可能• ホスト言語側でゲスト言語の表現式を合成することで、単なる関数呼び出し以上の表現が可能

34
13年7月9日火曜日

例：関数double
functionsdouble : int -> int
double(x) == x * 2
引数の２倍を返す関数

35
13年7月9日火曜日

例：double(10)をSmalltalkで評価する

VDM仕様

VDM関数をSmalltalkクロージャとして呼び出す
10 * 2 = 20

36
13年7月9日火曜日

例：Smalltalkのクロージャとしての
VDM double関数
Smalltalkのクロージャ

VDM仕様

VDM関数
37
13年7月9日火曜日

応用：ライブUIプロトタイピング環境
Lively Walk-Through
スケッチング
ツール
UIのスケッチ画像

VDM仕様

GUI部品
イベントログ

合意事項の記述
38

13年7月9日火曜日

Conclusion

39
13年7月9日火曜日

まとめ• 軽量形式手法とUIデザイン• UIデザイナと形式仕様技術者の対話としてのライブUIプロトタイピング• VDM-SLでライブプログラミング

13年7月9日火曜日§

情報隠蔽を破るバックドア§

実行時改変と継続実行§

自由度の高いFFI

40

今後の課題• さらにo

生き生きとしたo

技術者やデザイナの間で会話が進むo

多様なUI形態のデザインに使える（タッチデバイス、ウェブUI、Kinect等）

o

使っていて楽しい環境をめざします41
13年7月9日火曜日

Thank you.

42
13年7月9日火曜日