diff --git a/courseA/Alloy.html b/courseA/Alloy.html index b886006..283e0fa 100644 --- a/courseA/Alloy.html +++ b/courseA/Alloy.html @@ -29,7 +29,7 @@

記述した仕様を仮想的に実行したり，コンピュータを用いて解析を行うことができる

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

@@ -67,14 +67,14 @@

Alloy による記述例:

以下の仕様記述では名前の集合を Name，アドレスの集合を Addr，アドレス帳の集合を Book で表しています．
- sig でこれらの集合を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，インスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが異なると考えてください．
+ sig でこれらの集合を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，インスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが別々になると考えてください．
Book は，2つのフィールド owner と addr を持っています．Alloy におけるフィールドは，インスタンスの内部構造を表すものではなく，基本的に2つの集合の要素間の関係を表しています．たとえば Book の owner フィールドは，Book の各要素に Name の要素を対応づける関係を表しています．フィールドの詳細な意味については後ほど説明します．

Alloy では，操作も関係で表されます．たとえば add 操作は，連絡先を登録する前の Book の状態と，登録した後の Book の状態の間の関係を表していると考えます．
より具体的には pred を用いて，登録前の Book の状態 b，登録後の Book の状態 b'，登録する連絡先の名前 n，登録するアドレス a の間に成り立つ述語として定義されています．
述語の本体は 1つ以上の式によって構成されます．これらの式は変数間に成り立つ制約関係を表しているため記述順は関係ありません．たとえば，b'.owner = b.owner は，add 操作前の Book の owner と，add 操作後の Book の owner が同じであることを示しています． - b'.addr = b.addr + n -> a は，add 操作前の Book の addr （Book の各インスタンスが持つ，名前とアドレスの対応表）に，名前 n とアドレス a の対応を付け足したものが，add 操作後の Book の addr になることを示しています．これらの式は順番を入れ替えても意味は変わりません． + b'.addr = b.addr + n -> a は，add 操作前の Book の addr （Book の各インスタンスが持つ，名前とアドレスの対応表）に対して，名前 n とアドレス a の対応を付け足したものが，add 操作後の Book の addr になることを示しています．これらの式は順番を入れ替えても意味は変わりません．

実行は，run で指定された述語を呼び出すことによってなされます．ここでは，execute という引数を持たない述語が呼び出されます．
@@ -85,7 +85,7 @@ ここでは，b0, b1, b2, b3 という Book のインスタンスのある組み合わせにおいて（disj がついているのでこれら4つのインスタンスは互いに異なります），また，n0, n1, n2 という Name の互いに異なる3つのインスタンスのある組み合わせについて，さらに，a0, a1 という Addr の互いに異ならなくてもよいインスタンスのある組み合わせについて，| 以下の論理式が成り立っていることを示しています．| 以下の論理式は { と } で囲まれている4つの論理式をまとめたもの，すなわち4つの論理式が同時に成り立っていることを示す1つの論理式になります．
この4つの論理式も同時に成り立っているので，記述の順序を変えても意味は変わらないのですが，しかし，実行において最初に init 操作が呼ばれて，次に add 操作が2回呼ばれ，最後に del 操作が呼ばれることを表しています． - 詳細は後ほど説明しますが，これには，Book の4つのインスタンスが関係しています．まず初期化の操作 init に関わるのは b0 です．次に，最初の add 操作は，b0 を b1 に変更します． + 詳細は後ほど説明しますが，これには，Book の4つのインスタンス（b0, b1, b2, b3）が関係しています．まず初期化の操作 init に関わるのは b0 です．次に，最初の add 操作は，b0 を b1 に変更します．さらに，次の add 操作は，b1 を b2 に，最後の del 操作は b2 を b3 に変更します．このようにインスタンス（の状態）を受け渡すことによって，実行が進んでいくことを表すことができます．

@@ -131,7 +131,7 @@

- 可視化では実行時に生成される1つのインスタンスが，1つの矩形で表されます．たとえば，図の上部に並んでいる4つの矩形は，execute 述語内で宣言されている4つの変数，b0, b1, b2, b3に対応しています． + 可視化では実行時に生成される1つのインスタンスが，1つの矩形で表されます．たとえば，図の上部に並んでいる4つの矩形は，execute 述語内で宣言されている4つの変数，b0, b1, b2, b3が参照する Book の4つのインスタンスに対応しています．矩形内部には，そのインスタンスが所属しているクラス名とインスタンスのIDが記されています．また，括弧の中にはそのインスタンスを参照している変数名が記されています．
Book のインスタンスは4つありますが，これは手続き型プログラムで考えると Book の1つのインスタンスの状態が3回変わったことに相当しています． Book の初期化後の状態が Book3，最初の add 操作後の状態が Book2，次の add 操作後の状態が Book1，最後の del 操作後の状態が Book0 に当たります． diff --git a/courseA/DTRAM.html b/courseA/DTRAM.html index da54b77..457a669 100644 --- a/courseA/DTRAM.html +++ b/courseA/DTRAM.html @@ -25,33 +25,33 @@ 形式的アーキテクチャ記述言語とは，システム全体の構造を箱や線などの図ではなく，厳密に意味が定義された言語の形式で記述する方法です．形式的アーキテクチャ記述言語では一般に，

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

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

DTRAM とは？

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

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

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

DTRAM による仕様記述:

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

@@ -73,7 +73,8 @@

DTRAM による記述例:

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

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

メッセージを受け取ったリソースは状態遷移を行います．各リソースの状態遷移は状態遷移関数によって定義されます． - たとえば，Add チャンネルでメッセージを受け取った book.addr リソースの状態遷移は，状態遷移関数 book.addr(pre_addr: Map, add(name: Str, addr: Str)) = insert(pre_addr, name, addr) によって定義されています．
- 状態遷移関数の関数名にはリソース名をそのまま用います．状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ たとえば，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引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です． - したがって，上の式の右辺は，遷移前の状態 prev_addr に，メッセージ add() の引数で渡された name と addr の対応を追加したものが遷移後の状態になることを示しています．
+ したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
なお，変数名の右側の : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．状態の型が，List，Map，Json であるリソースは子リソースを持つことができます．

@@ -114,7 +118,7 @@

実行の可視化:

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

@@ -130,13 +134,13 @@

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

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

@@ -151,7 +155,8 @@

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

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

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

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

-【酒屋の在庫管理システムの仕様説明】へ +【酒屋の在庫管理システムの仕様説明】へ \ No newline at end of file diff --git a/courseB/Alloy.html b/courseB/Alloy.html new file mode 100644 index 0000000..283e0fa --- /dev/null +++ b/courseB/Alloy.html @@ -0,0 +1,161 @@ + + + + + + 【Alloyの説明】 + + +

【Alloy の概要説明】

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

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

+ Alloy は代表的な形式的仕様記述言語の一つです．
+ 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
+

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

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

Alloy とは？

+ Alloy は形式的仕様記述言語としては比較的表現能力が高いため，完全に網羅的な解析はできませんが，実用性を大きく損なわない範囲で網羅性を制限した解析を行うことができるといった特長があります．
+ 本実験では，Alloy による仕様記述と仕様の仮想実行に着目していきます．そのため，Alloy による仕様の解析は行いません．また，Alloy のツールをPCにダウンロードして操作していただく必要もありません．
+

Alloyによる仕様記述:

+ Alloy では，集合と関係を使って仕様を記述していきます．また，その記述は宣言的な形式で行われます．
+ 宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ, + 記述された順に実行されていきます．
+ 一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います． + 連立方程式では，すべての式が同時に成り立っているため，式の記述順に関係なく同じ解が得られます．そのため，宣言的記述には基本的に時間の経過が存在しません．実行の初期状態から最終状態までのすべての状態が同時に存在していることになります．
+ Alloy の概念的な説明はこれくらいにして，具体的に Alloy の記述を見ていきましょう． +

Alloy による仕様記述の例

例題仕様:

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

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

Alloy による記述例:

+ 以下の仕様記述では名前の集合を Name，アドレスの集合を Addr，アドレス帳の集合を Book で表しています．
+ sig でこれらの集合を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，インスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが別々になると考えてください．
+ Book は，2つのフィールド owner と addr を持っています．Alloy におけるフィールドは，インスタンスの内部構造を表すものではなく，基本的に2つの集合の要素間の関係を表しています．たとえば Book の owner フィールドは，Book の各要素に Name の要素を対応づける関係を表しています．フィールドの詳細な意味については後ほど説明します．
+

+ Alloy では，操作も関係で表されます．たとえば add 操作は，連絡先を登録する前の Book の状態と，登録した後の Book の状態の間の関係を表していると考えます．
+ より具体的には pred を用いて，登録前の Book の状態 b，登録後の Book の状態 b'，登録する連絡先の名前 n，登録するアドレス a の間に成り立つ述語として定義されています．
+ 述語の本体は 1つ以上の式によって構成されます．これらの式は変数間に成り立つ制約関係を表しているため記述順は関係ありません．たとえば，b'.owner = b.owner は，add 操作前の Book の owner と，add 操作後の Book の owner が同じであることを示しています． + b'.addr = b.addr + n -> a は，add 操作前の Book の addr （Book の各インスタンスが持つ，名前とアドレスの対応表）に対して，名前 n とアドレス a の対応を付け足したものが，add 操作後の Book の addr になることを示しています．これらの式は順番を入れ替えても意味は変わりません． +

+ 実行は，run で指定された述語を呼び出すことによってなされます．ここでは，execute という引数を持たない述語が呼び出されます．
+ execute の本体については，いくつか説明が必要です．
+ まず，この execute 本体は，1つの論理式で構成されています．一見，4つの論理式が列挙されているように思いますが，全体として論立式は1つです．
+ ポイントは存在限量子 some です．some は，後ろに並んだ変数の値のある組み合わせにおいて，| の後ろに記載された論理式が成り立つということを示しています．似たようなものに all と no があります． + all は，後ろに並んだ変数の値の任意の組み合わせにおいて，| の後ろの論理式が成り立つということを，no は，後ろに並んだ変数の値のどんな組み合わせにおいても，| の後ろの論理式が成り立たないことを示します．
+ ここでは，b0, b1, b2, b3 という Book のインスタンスのある組み合わせにおいて（disj がついているのでこれら4つのインスタンスは互いに異なります），また，n0, n1, n2 という Name の互いに異なる3つのインスタンスのある組み合わせについて， + さらに，a0, a1 という Addr の互いに異ならなくてもよいインスタンスのある組み合わせについて，| 以下の論理式が成り立っていることを示しています．| 以下の論理式は { と } で囲まれている4つの論理式をまとめたもの，すなわち4つの論理式が同時に成り立っていることを示す1つの論理式になります．
+ この4つの論理式も同時に成り立っているので，記述の順序を変えても意味は変わらないのですが，しかし，実行において最初に init 操作が呼ばれて，次に add 操作が2回呼ばれ，最後に del 操作が呼ばれることを表しています． + 詳細は後ほど説明しますが，これには，Book の4つのインスタンス（b0, b1, b2, b3）が関係しています．まず初期化の操作 init に関わるのは b0 です．次に，最初の add 操作は，b0 を b1 に変更します． + さらに，次の add 操作は，b1 を b2 に，最後の del 操作は b2 を b3 に変更します．このようにインスタンス（の状態）を受け渡すことによって，実行が進んでいくことを表すことができます． +

+sig Name, Addr {}
+sig Book {
+	owner: Name,
+	addr: Name -> lone Addr
+}
+
+pred init[b: Book, n: Name] {
+	b.owner = n
+	no b.addr
+}
+
+pred add[b, b': Book, n: Name, a: Addr] {
+	b'.owner = b.owner
+	b'.addr = b.addr + n -> a
+}
+
+pred del[b, b': Book, n: Name] {
+	b'.owner = b.owner
+	b'.addr = b.addr - n -> b.addr[n]
+}
+
+pred execute[] {
+	some disj b0, b1, b2, b3: Book, disj n0, n1, n2: Name, a0, a1: Addr | {
+		init[b0, n0]
+		add[b0, b1, n1, a0]
+		add[b1, b2, n2, a1]
+		del[b2, b3, n1]
+	}
+}
+
+run execute for 2 but 4 Book, 3 Name
+

実行の可視化:

+ Alloy では実行を可視化することができます．上の仕様記述内の run による実行を可視化したものが以下の図です． +

+ 可視化では実行時に生成される1つのインスタンスが，1つの矩形で表されます．たとえば，図の上部に並んでいる4つの矩形は，execute 述語内で宣言されている4つの変数，b0, b1, b2, b3が参照する Book の4つのインスタンスに対応しています． + 矩形内部には，そのインスタンスが所属しているクラス名とインスタンスのIDが記されています．また，括弧の中にはそのインスタンスを参照している変数名が記されています．
+ Book のインスタンスは4つありますが，これは手続き型プログラムで考えると Book の1つのインスタンスの状態が3回変わったことに相当しています． + Book の初期化後の状態が Book3，最初の add 操作後の状態が Book2，次の add 操作後の状態が Book1，最後の del 操作後の状態が Book0 に当たります． + Alloy は宣言型言語なので，これらは順番に生成されるというわけではなく，最初から同時に存在しています．
+

+ Book の owner フィールドは，Book の要素と，Name の要素の間の関係として定義されます． + Book のインスタンスを1つ指定すれば，ownerフィールドを使って b.owner のように Name のインスタンスを1つ取ってくることができるためです． + この図では，Book のどのインスタンスも同じ Name のインスタンスを参照しています．これは，この実行における Book の状態の変化では，owner が変わらないためです．
+

+ addr フィールドは少し複雑です．この仕様では addr フィールドは，addr: Name -> lone Addr のように定義されています． + これは，addr フィールドが Name から Addr への対応関係を参照していることを表しています． + ここで，lone の記述は Name の各要素に対して，対応する Addr がたかだか1つ（0個か1個）であることを示しています．
+ たとえば，Book2 を見ると，addr は Name1 に Addr1 を対応させていることがわかります． + 一方，Name0 に対応する Addr の要素は存在していません．Book1 では add 操作によって，新たに Name0 から Addr0 への対応が追加されています． + さらに Book0 ではadd 操作によって，Name1 から Addr1 への対応が削除されています．
+

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

+
+【DTRAM の概要説明】へ + + + \ No newline at end of file diff --git a/courseB/DTRAM.html b/courseB/DTRAM.html new file mode 100644 index 0000000..457a669 --- /dev/null +++ b/courseB/DTRAM.html @@ -0,0 +1,193 @@ + + + + + + 【DTRAMの説明】 + + +

【DTRAM の概要説明】

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

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

+ DTRAM は仕様とアーキテクチャの両方を同時に記述することが可能な言語で，形式的仕様記述言語であると同時に形式的アーキテクチャ記述言語でもあります．
+ 形式的アーキテクチャ記述言語とは，システム全体の構造を箱や線などの図ではなく，厳密に意味が定義された言語の形式で記述する方法です．形式的アーキテクチャ記述言語では一般に，
+

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

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

DTRAM とは？

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

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

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

DTRAM による仕様記述:

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

DTRAM による仕様記述の例

例題仕様:

+ Alloy のときに記述したアドレス帳と同じ仕様を，今度は 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引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
+ この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です． + したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
+ なお，変数名の右側の : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．状態の型が，List，Map，Json であるリソースは子リソースを持つことができます． +

+ Alloy と異なり，DTRAM では仮想実行に関する情報を仕様記述には記載しません． +

+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 でも実行を可視化することができます．Alloy とは異なり，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 ではこのようにして実行が可視化されます． +

+
+【酒屋の在庫管理システムの仕様説明】へ + + + \ No newline at end of file diff --git a/courseC/Alloy.html b/courseC/Alloy.html new file mode 100644 index 0000000..e0de446 --- /dev/null +++ b/courseC/Alloy.html @@ -0,0 +1,147 @@ + + + + + + 【Alloyの説明】 + + +

【Alloy の概要説明】

Alloy とは？

+ Alloy は代表的な形式的仕様記述言語の一つです．
+ Alloy は形式的仕様記述言語としては比較的表現能力が高いため，完全に網羅的な解析はできませんが，実用性を大きく損なわない範囲で網羅性を制限した解析を行うことができるといった特長があります．
+ 本実験では，Alloy による仕様記述と仕様の仮想実行に着目していきます．そのため，Alloy による仕様の解析は行いません．また，Alloy のツールをPCにダウンロードして操作していただく必要もありません．
+

Alloyによる仕様記述:

+ Alloy では，集合と関係を使って仕様を記述していきます．また，その記述は宣言的な形式で行われます．
+ 宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ, + 記述された順に実行されていきます．
+ 一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います． + 連立方程式では，すべての式が同時に成り立っているため，式の記述順に関係なく同じ解が得られます．そのため，宣言的記述には基本的に時間の経過が存在しません．実行の初期状態から最終状態までのすべての状態が同時に存在していることになります．これは DTRAM の記述にはなかった性質です．
+ Alloy の概念的な説明はこれくらいにして，具体的に Alloy の記述を見ていきましょう． +

Alloy による仕様記述の例

例題仕様:

+ DTRAM のときに記述したアドレス帳と同じ仕様を，今度は Alloy を用いて記述することを考えます． + アドレス帳の仕様を再掲します． +

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

Alloy による記述例:

+ 以下の仕様記述では名前の集合を Name，アドレスの集合を Addr，アドレス帳の集合を Book で表しています．
+ sig でこれらの集合を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，DTRAM とは異なりインスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが別々になると考えてください．
+ Book は，2つのフィールド owner と addr を持っています．Alloy におけるフィールドは，インスタンスの内部構造を表すものではなく，基本的に2つの集合の要素間の関係を表しています．たとえば Book の owner フィールドは，Book の各要素に Name の要素を対応づける関係を表しています．フィールドの詳細な意味については後ほど説明します．
+

+ Alloy では実行は，run で指定された述語を呼び出すことによってなされます．ここでは，execute という引数を持たない述語が呼び出されます．
+ execute の本体については，いくつか説明が必要です．
+ まず，この execute 本体は，1つの論理式で構成されています．一見，4つの論理式が列挙されているように思いますが，全体として論立式は1つです．
+ ポイントは存在限量子 some です．some は，後ろに並んだ変数の値のある組み合わせにおいて，| の後ろに記載された論理式が成り立つということを示しています．似たようなものに all と no があります． + all は，後ろに並んだ変数の値の任意の組み合わせにおいて，| の後ろの論理式が成り立つということを，no は，後ろに並んだ変数の値のどんな組み合わせにおいても，| の後ろの論理式が成り立たないことを示します．
+ ここでは，b0, b1, b2, b3 という Book のインスタンスのある組み合わせにおいて（disj がついているのでこれら4つのインスタンスは互いに異なります），また，n0, n1, n2 という Name の互いに異なる3つのインスタンスのある組み合わせについて， + さらに，a0, a1 という Addr の互いに異ならなくてもよいインスタンスのある組み合わせについて，| 以下の論理式が成り立っていることを示しています．| 以下の論理式は { と } で囲まれている4つの論理式をまとめたもの，すなわち4つの論理式が同時に成り立っていることを示す1つの論理式になります．
+ この4つの論理式も同時に成り立っているので，記述の順序を変えても意味は変わらないのですが，しかし，実行において最初に init 操作が呼ばれて，次に add 操作が2回呼ばれ，最後に del 操作が呼ばれることを表しています． + 詳細は後ほど説明しますが，これには，Book の4つのインスタンス（b0, b1, b2, b3）が関係しています．まず初期化の操作 init に関わるのは b0 です．次に，最初の add 操作は，b0 を b1 に変更します． + さらに，次の add 操作は，b1 を b2 に，最後の del 操作は b2 を b3 に変更します．このようにインスタンス（の状態）を受け渡すことによって，実行が進んでいくことを表すことができます． +

+sig Name, Addr {}
+sig Book {
+	owner: Name,
+	addr: Name -> lone Addr
+}
+
+pred init[b: Book, n: Name] {
+	b.owner = n
+	no b.addr
+}
+
+pred add[b, b': Book, n: Name, a: Addr] {
+	b'.owner = b.owner
+	b'.addr = b.addr + n -> a
+}
+
+pred del[b, b': Book, n: Name] {
+	b'.owner = b.owner
+	b'.addr = b.addr - n -> b.addr[n]
+}
+
+pred execute[] {
+	some disj b0, b1, b2, b3: Book, disj n0, n1, n2: Name, a0, a1: Addr | {
+		init[b0, n0]
+		add[b0, b1, n1, a0]
+		add[b1, b2, n2, a1]
+		del[b2, b3, n1]
+	}
+}
+
+run execute for 2 but 4 Book, 3 Name
+

実行の可視化:

+ Alloy でも実行を可視化することができます．DTRAM とは異なり，Alloy では上の仕様記述内の run による実行を一枚の図で可視化します（以下の図参照）． +

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

+
+【酒屋の在庫管理システムの仕様説明】へ + + + \ No newline at end of file diff --git a/courseC/DTRAM.html b/courseC/DTRAM.html new file mode 100644 index 0000000..72a3507 --- /dev/null +++ b/courseC/DTRAM.html @@ -0,0 +1,203 @@ + + + + + + 【DTRAMの説明】 + + +

【DTRAM の概要説明】

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

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

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

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

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

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

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

DTRAM とは？

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

DTRAM による仕様記述:

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

DTRAM による仕様記述の例

例題仕様:

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

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

DTRAM による記述例:

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

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

+ によって定義されています．
+ 少しわかりにくいですが，この式では左端の book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．
+ また関数 book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
+ この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です． + したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
+ なお，変数名の右側の : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．状態の型が，List，Map，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 のツールを用いてインタラクティブに仮想実行を進めていきます．まず，システムの初期状態を可視化したものが以下の図です， +

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

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

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

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

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

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

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

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

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

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

+
+【Alloy の概要説明】へ + + + \ No newline at end of file diff --git a/courseD/Alloy.html b/courseD/Alloy.html new file mode 100644 index 0000000..e0de446 --- /dev/null +++ b/courseD/Alloy.html @@ -0,0 +1,147 @@ + + + + + + 【Alloyの説明】 + + +

【Alloy の概要説明】

Alloy とは？

Alloyによる仕様記述:

+ Alloy では，集合と関係を使って仕様を記述していきます．また，その記述は宣言的な形式で行われます．
+ 宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ, + 記述された順に実行されていきます．
+ 一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います． + 連立方程式では，すべての式が同時に成り立っているため，式の記述順に関係なく同じ解が得られます．そのため，宣言的記述には基本的に時間の経過が存在しません．実行の初期状態から最終状態までのすべての状態が同時に存在していることになります．これは DTRAM の記述にはなかった性質です．
+ Alloy の概念的な説明はこれくらいにして，具体的に Alloy の記述を見ていきましょう． +

Alloy による仕様記述の例

例題仕様:

+ DTRAM のときに記述したアドレス帳と同じ仕様を，今度は Alloy を用いて記述することを考えます． + アドレス帳の仕様を再掲します． +

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

Alloy による記述例:

+sig Name, Addr {}
+sig Book {
+	owner: Name,
+	addr: Name -> lone Addr
+}
+
+pred init[b: Book, n: Name] {
+	b.owner = n
+	no b.addr
+}
+
+pred add[b, b': Book, n: Name, a: Addr] {
+	b'.owner = b.owner
+	b'.addr = b.addr + n -> a
+}
+
+pred del[b, b': Book, n: Name] {
+	b'.owner = b.owner
+	b'.addr = b.addr - n -> b.addr[n]
+}
+
+pred execute[] {
+	some disj b0, b1, b2, b3: Book, disj n0, n1, n2: Name, a0, a1: Addr | {
+		init[b0, n0]
+		add[b0, b1, n1, a0]
+		add[b1, b2, n2, a1]
+		del[b2, b3, n1]
+	}
+}
+
+run execute for 2 but 4 Book, 3 Name
+

実行の可視化:

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

+
+【酒屋の在庫管理システムの仕様説明】へ + + + \ No newline at end of file diff --git a/courseD/DTRAM.html b/courseD/DTRAM.html new file mode 100644 index 0000000..72a3507 --- /dev/null +++ b/courseD/DTRAM.html @@ -0,0 +1,203 @@ + + + + + + 【DTRAMの説明】 + + +

【DTRAM の概要説明】

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

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

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

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

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

DTRAM とは？

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

DTRAM による仕様記述:

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

DTRAM による仕様記述の例

例題仕様:

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

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

DTRAM による記述例:

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

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

+ によって定義されています．
+ 少しわかりにくいですが，この式では左端の book.addr が関数名に相当します．状態遷移関数の関数名にはリソース名をそのまま用います．
+ また関数 book.addr は，2つの引数を受け取っています．DTRAMでは，状態遷移関数の第1引数は遷移前の状態，第2引数は受け取るメッセージ，式の右辺は遷移後の状態を表しています．
+ この例では，メッセージ add(name, addr) を受け取った book.addr リソースが，状態を pre_addr から insert(pre_addr, name, addr) に変化させることが示されています．
+ この insert() 関数は，第1引数に渡された写像(対応表)に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です． + したがって，上の式の右辺は，遷移前の状態 prev_addr に対して，メッセージ add() の引数で渡された name と addr の対応を追加した写像が遷移後の状態になることを示しています．
+ なお，変数名の右側の : の直後に変数の型を記述することができます．型推論によって型がわかる場合には，型を省略することもできます．状態の型が，List，Map，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)
+}
+

実行の可視化:

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

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

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

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

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

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

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

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

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

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

+
+【Alloy の概要説明】へ + + + \ No newline at end of file