diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html index b26d31c..acaceb1 100644 --- a/courseA/IM_Alloy.html +++ b/courseA/IM_Alloy.html @@ -46,7 +46,7 @@ receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と， 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス it' が存在していることを示しており， - 直観的には Item のインスタンスの生成を示しています．
+ 直観的には，Item のインスタンスが，出荷か入荷を行うことによって複製されたことを示しています．
最後の execute では，init ，itemRegistraction ，receivingOrShipping を この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います． diff --git a/courseA/IM_DTRAM.html b/courseA/IM_DTRAM.html index 3d3e8ad..412805d 100644 --- a/courseA/IM_DTRAM.html +++ b/courseA/IM_DTRAM.html @@ -66,7 +66,7 @@ この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
図の中央にある inventory リソースは ItemRegistration チャンネルから商品を登録するメッセージを受け取ります．
inventory リソースの子リソースである，inventory.{itemId} リソースは商品を表しています．
- このリソース名に含まれる itemId は商品IDを表すパスパラメータで，一意な商品の特定を可能にしています．
+ このリソース名に含まれる itemId は商品idを表すパスパラメータで，一意な商品の特定を可能にしています．
inventory.{itemId} リソースの子リソースである inventory.{itemId}.count リソースは inventory.{itemId} の在庫数を表しており， ReceivingOrShipping チャンネルから入荷もしくは出荷を行うメッセージを受け取ります．

@@ -107,7 +107,7 @@

registerItem メッセージのシグニチャが表示されます．
- itemId は商品ID，itemName は商品名 ，quantity は初期数量を表します． + itemId は商品id，itemName は商品名 ，quantity は初期数量を表します．

diff --git a/courseA/ST_DTRAM.html b/courseA/ST_DTRAM.html index a6e560b..70b2cdf 100644 --- a/courseA/ST_DTRAM.html +++ b/courseA/ST_DTRAM.html @@ -31,14 +31,13 @@
  • accounts.{accountId}: accountId で登録されているアカウント
  • accounts.{accountId}.name: accountId で示されたアカウントのアカウント名
  • accounts.{accountId}.tweets: accountId で示されたアカウントのツイートリスト
    • -
  • accounts.{accountId}.tweets.{tid}: accountId で示されたアカウントのツイートリストに tid で登録されているツイート
    • +
  • accounts.{accountId}.tweets.{tid}: accountId で示されたアカウントのツイートリストの tid 番目のツイート
    • DTRAM では，SimpleTwitter のモデルを以下のようなチャンネル単位で記述していきます．
    アカウント登録用のイベントチャンネルを Signup ，accountId で登録されているアカウントに対してツイートを行うためのイベントチャンネルを Tweet(accountId:Str) として宣言しています．
    Signup チャンネルでは accounts リソースが，メッセージ signUp(accountId, name) を受け取ると， リソースの状態が accountDB から insert(accountDB, accountId, {"name": name, "tweets": nil}) に変わることを示しています．nil は空のマップやリストを表しています．
    -ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．
    -また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．
    +ここで，insert() 関数は，第1引数に渡された写像に対し，第2引数と第3引数の対応を追加した結果得られる写像を返す関数です．また {"name": name, "tweets": nil} は，"name" と "tweets" をキーに持つ JSON オブジェクトを表しています．
    Tweet(accountId:Str) チャンネルでは accounts.{accountId}.tweets リソースがメッセージ tweet(contents) を受け取ると， 遷移前の状態 tweetList が append(tweetList, contents) に変わることを示しています．
    ここで，append() 関数は，第1引数に渡されたリストに対し，第2引数のオブジェクトを末尾に追加した結果得られるリストを返す関数です．
    @@ -68,7 +67,7 @@ この図がモデルの実行に依らない，リソースとチャンネルの関係を表していることに注意して下さい．
    図の中央にある accounts リソースは Signup チャンネルからアカウントを登録するメッセージを受け取ります．
    accounts リソースの子リソースである，accounts.{accountId} リソースはアカウントを表しています．
    - リソース名に含まれる accountId はアカウントIDを表すパスパラメータで，一意なアカウントの特定を可能にしています．
    + このリソース名に含まれる accountId はアカウントidを表すパスパラメータで，一意なアカウントの特定を可能にしています．
    accounts.{accountId} リソースの子リソースである accounts.{accountId}.tweets リソースは accounts.{accountId} のツイートリストを表しており， Tweet チャンネルからツイートを行うメッセージを受け取ります．

    @@ -78,7 +77,7 @@

    ここでは，SimpleTwitter モデルの仮想実行について説明します．この仮想実行で用いるテストケースは次の通りです．

      -
    1. accounts にアカウント名が "Satou" という新しいアカウントをアカウントID @123 で登録します．
      2. +
    2. accounts にアカウント名が "Satou" という新しいアカウントをアカウントid @123 で登録します．
    3. 登録したアカウント(Satou)で "Hello" というツイートを行います．

    @@ -109,7 +108,7 @@

    signUp メッセージのシグニチャが表示されます．
    - accountId はアカウントID，name はアカウント名を表します． + accountId はアカウントid，name はアカウント名を表します．