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 に当たります．