今日は 6.3 メディア資産管理のところからです iView MediaPro という実在のソフトウェアのモデル化をして粗を探すらしい…… 「このモデル化の動機は、もしかしたら今とは異なる設計があり得たのではないかと思えるような、嫌な体験を何度か経験したことであ…

今日は 6.2.4 ホテルの客室施錠のイベントに基づくモデル化のところです。 pred で記述していたチェックイン、入室、チェックアウトなどの操作を抽象シグネチャ Event を拡張したシグネチャとして定義して記述する方法 チェックイン後すぐ入室イベントがある…

今日は 6.2.3 ホテルの客室施錠の解析のところからです。 不正な入室がないことの assert 「客がある時刻に入室する(錠前を開ける)時、フロントでその部屋に*宿泊客が登録済みなら*その客が登録されている」 ちょっとまわりくどくなっているのは客室錠前のシ…

今日は 6.2 ホテルの客室施錠 からです。 「再コード可能錠」を使った使い捨て客室鍵の運用管理のシステムのモデル化 錠前が疑似乱数列を用いて「現在の鍵の組み合わせ」と「次の鍵の組み合わせ」を持っており、「次の鍵」で開かれると状態が更新される やは…

抽象によるソフトウェア設計−Alloyではじめる形式手法−作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫出版社/メーカー: オーム社発売日: 2011/07/15メディア: 単行本（ソフトカバー）購入: 8人 クリック: 274回この商品を含むブログ (35…

今日は 5.4 スコープの選択と単調性からです。 スコープの選びかたの指針 シグネチャの上限が宣言中の定数に見合う程度に多いこと シグネチャに関連するすべての値に明示的に名前がついている場合その変数の数をスコープにすれば充分 モデルの検証したい状態…

今日は 5.3 非限定の全称限量子からです。実は昨日もここを読んでいたのですが、読み解くのが難しくて昨日はメモを書けなかったのでした。 生成公理とスコープの爆発 集合を表すシグネチャ Set の論理和についての検査を書く sig Element {} sig Seg { eleme…

抽象によるソフトウェア設計−Alloyではじめる形式手法−作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫出版社/メーカー: オーム社発売日: 2011/07/15メディア: 単行本（ソフトカバー）購入: 8人 クリック: 274回この商品を含むブログ (35…

今日は第4章の 4.7 モジュールと多相性からです。 各ファイルの先頭でモジュール宣言(module) モジュール名とファイルパスは一致していないといけない(1モジュール=1ファイル) 他のモジュールのインポートは open で指定 open 参照する時に / のように / の…

今日は第4章の 4.5 ファクト、述語、関数、アサーションからです。 ファクト(fact) 常に成り立つべき制約 シグネチャの宣言の {} の中に書く制約はシグネチャファクトと呼ばれ fact で後で書くのと同等 シグネチャファクト内でフィールド名を展開したくない…

今日は第4章の 4.5 ファクト、述語、関数、アサーションからです。 ファクト(fact) 常に成り立つべき制約 シグネチャの宣言の {} の中に書く制約はシグネチャファクトと呼ばれ fact で後で書くのと同等 シグネチャファクト内でフィールド名を展開したくない…

今日は第4章の 4.4 型と型検査からです。 Alloy における型システムは、解析前のエラー検出と、フィールドのオーバーロードを解消(同じフィールド名がどのシグネチャのものかを解決する)に用いられる シグネチャには「基本型」がつけられる A1 が A の拡張シ…

またずいぶん間があいてしまいました。今日は第4章の 4.3 モデル図からです。言語の章にモデル図の説明とはこれいかに。多重度のキーワードの説明にモデル図を使うという意味のようです。 シグネチャと関係のそれぞれのモデル図での表記について シグネチャ…