【DTRAM の概要説明】

次に本実験で用いる DTRAM の概要について説明します．
現時点では本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．

形式的仕様記述言語とは？

DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
形式的仕様記述言語とは，仕様を自然言語ではなく，論理式や等式のような数学的に厳密に意味が定義された形式で記述する方法で，

仕様を曖昧性なく厳密に記述することができる，
プログラミング言語よりも高い抽象度でシステムの振る舞いを記述することができる，
記述した仕様を仮想的に実行したり，コンピュータを用いて解析を行うことができる

といった特長を持っています．
コンピュータによる仕様の解析としては，仕様レベルで不具合が存在しないか（機能的要件が満たされているか）を網羅的に調べたり，セキュリティホールが存在しないことを確認することなどが挙げられます．
形式的仕様記述言語による記述は，通常のプログラミング言語におけるソースコードの記述とはかなり異なっております．そのため，最初に形式的な仕様記述を見ると少々戸惑うかもしれません．
一般的に形式的仕様記述言語の表現能力はプログラミング言語よりも低く，表現能力が低くなればなるほど複雑な振る舞いが記述できなくなる一方で，強力な解析ができるといった関係が成り立っています．

アーキテクチャ記述言語とは？

形式的アーキテクチャ記述言語とは，システム全体の構造を箱や線などの図ではなく，厳密に意味が定義された言語の形式で記述する方法です．形式的アーキテクチャ記述言語では一般に，

システムの構成要素であるコンポーネント，
コンポーネント間の関係，
コンポーネント間のデータや制御の流れ

などが記述されます．
アーキテクチャ記述言語で記述されたアーキテクチャモデルは，システム全体のパフォーマンス，メモリ消費量や通信量，信頼性などの非機能的要件の予測や解析に用いられます．
また開発チーム内で，システムの全体構造についての理解を共有するためのドキュメントとしても利用されます．

DTRAM とは？

DTRAM は仕様とアーキテクチャの両方を形式的に記述することが可能な言語です．形式的仕様記述言語として見ると表現能力がかなり高いため，網羅的な解析はできません．
DTRAM では仕様そのものの解析より，

仕様の仮想実行による仕様レベルでのテスト，
記述したアーキテクチャで，記述した仕様が実現できるか否かのチェック，
通常のプログラミング言語で記述された実行可能なプロトタイプの自動生成

などを行うことを重視しています．
また，形式的アーキテクチャ記述言語としては記述の抽象度が高いため，同一のアーキテクチャ記述からさまざまな設計を持ったプロトタイプの実装を導出することができます．本実験では，DTRAM による仕様記述と仕様の仮想実行に着目していきます．そのため，DTRAM によるアーキテクチャのチェックやプロトタイプの自動生成は行いません．また，DTRAM のツールをPCにダウンロードして操作していただく必要もありません．

DTRAM による仕様記述:

DTRAM では，リソースとチャンネルを使って仕様とアーキテクチャを記述していきます．
DTRAM におけるリソースとは，システムの外部から見えるデータのことです．Web サービスにおいて URL でアクセスされるリソースとほぼ同じものと考えて差し支えありません．DTRAM においてもリソースは階層構造を持つことができます．
チャンネルはリソースとリソースの間の通信路です．システム外部からの入力はイベントチャンネルと呼ばれる特殊なチャンネルによって受け付けられます．
リソースはチャンネルからメッセージを受け取ると状態遷移を行います．そのため，リソースは状態を持ちます．それでは，具体的に DTRAM の記述を見ていきましょう．

DTRAM による仕様記述の例

例題仕様:

簡単なアドレス帳の仕様を DTRAM で記述することを考えます．アドレス帳の仕様は次の通りです．

システムはアドレス帳を1つ持つ．
アドレス帳には所有者の名前が記載されている．
アドレス帳には連絡先の名前とアドレスの対応を任意個登録することができる．
アドレス帳において連絡先の名前が重複してはならない．
アドレス帳は連絡先の名前とアドレスの対応が1つも登録されていない状態を初期状態とする．
add 操作によって，指定した名前と指定したアドレスの対応をアドレス帳に登録することができる．
del 操作によって，指定した名前と対応するアドレスをアドレス帳から削除することができる．

DTRAM による記述例:

DTRAM では，チャンネル単位で仕様を記述していきます．たとえばリソースに対する操作毎に，イベントチャンネルを定義していきます．ここでは，初期化操作用のイベントチャンネルを Init，add 操作用のイベントチャンネルを Add，del 操作用のイベントチャンネルを Del とします．
channel でこれらのチャンネルを宣言します．チャンネルの宣言の中の out は，チャンネルを流れるメッセージを受け取るリソースを示しています．チャンネルにメッセージを送信するリソースも記述することができますが，本実験では使用しません．
DTRAM には，メインメソッドやメインスレッドに相当するものはなく，いずれかのイベントチャンネルが外部からのメッセージを受信するたびに状態遷移を行い，状態遷移後は次のメッセージが外部から入力されるまで何もせず待機します．リソースについては次に説明します．

DTRAM では，Web サービスと同様に階層化されたリソースを扱うことができます．リソースは状態を持ち，その状態を変更することができます．アドレス帳の仕様は次のような階層化されたリソースで表すこととします．

book：アドレス帳全体
book.owner：アドレス帳の所有者
book.addr：アドレス帳に記載された連絡先の名前と住所の対応表
book.addr.{name}：連絡先の名前 name に対応した住所

下の仕様記述を見るとわかると思いますが，チャンネル Init を流れるメッセージを受け取るリソースは book.owner です．同様に，チャンネル Add 内のメッセージを受け取るリソースは book.addr，チャンネル Del 内のメッセージを受け取るリソースも book.addr になります．

メッセージを受け取ったリソースは状態遷移を行います．各リソースの状態遷移は状態遷移関数によって定義されます．たとえば，Add チャンネルでメッセージを受け取った book.addr リソースの状態遷移は，状態遷移関数

book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr)

によって定義されています．
少しわかりにくいですが，この式では左端の book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．
また関数 book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
すなわち，r(x, y) = z と定義されていた場合，リソース r はメッセージ y を受け取ると，状態を x から z に変化させることを意味しています．
この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
なお，変数名の右側の : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．
状態の型が，List，Map，Json であるようなリソースは子リソースを持つことができます．ここで，List はリスト型，Map は写像型（キーと値の対応），Json はJSONオブジェクト型を表します．

channel Init {
	out book.owner(pre_name: Str, init(name: Str)) = name
}

channel Add {
	out book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr)
}

channel Del {
	out book.addr(pre_addr, del(name: Str)) = delete(pre_addr, name)
}

実行の可視化:

DTRAM では実行を可視化することができます．DTRAM のツールを用いてインタラクティブに仮想実行を進めていきます．まず，システムの初期状態を可視化したものが以下の図です，

可視化では1つのリソースが，1つの楕円で表されます．子リソースは親リソースの内側の領域に表示されます．リソースの上部にはリソース名が記され，リソースの中心にはリソースの現在の状態が記されています．

DTRAM の仮想実行では，メッセージを送りたいリソースをダブルクリックします．まず，book.owner リソースに，Init チャンネルを通じて，init("Suzuki") というメッセージを送ることを考えます．
book.owner リソースをダブルクリックします．

リソースに送信するメッセージの種類を選択する画面が表示されるので，init を選択します．

次にリソースに送信するメッセージの内容を入力します．ここでは，init("Suzuki") を入力します．

次の状態に遷移します．book.owner リソースの状態が，"Suzuki" に変わったことが分かります．

同様にして，book.addr リソースをダブルクリックして，Add チャンネルを通じて，add("Satou", "Tokyo") というメッセージを送ります．

book.addr リソースの子リソースとして，book.addr.Satou リソースが追加されたことが分かります．
また，book.addr.Satou リソースの状態が，"Tokyo" になっていることも分かります．

さらに，book.addr リソースをダブルクリックして，add("Tanaka", "Osaka") というメッセージを送ります．

book.addr リソースの子リソースとして，さらに book.addr.Tanaka リソースが追加され，その状態は "Osaka" になっています．

次に，book.addr リソースをダブルクリックして， del("Satou") というメッセージを送ります．

del を選択して， del("Satou") を入力します．

book.addr.Satou リソースが削除されました．

DTRAM ではこのようにして実行が可視化されます．

【ツイートシステム(SimpleTwitter) の概要説明】へ