今日は 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 モデル図からです。言語の章にモデル図の説明とはこれいかに。多重度のキーワードの説明にモデル図を使うという意味のようです。 シグネチャと関係のそれぞれのモデル図での表記について シグネチャ…

今日はシグネチャの宣言について sig A {} - トップレベルシグネチャ sig A1 extends A {} で A の部分シグネチャ、拡張シグネチャをを宣言 同じシグネチャの拡張シグネチャどおしは互いに素 abstract sig A {} とすると A は直接要素を持たずかならずいずれ…

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

ようやく第3章を終えます。今日は 3.7 「濃度制約と整数」。 関係に演算子 # を適用すると、タプルの数が得られる 整数の演算には plus, minus, mul, div, rem が利用できる Alloy では集合(関係)のほうが主役なので、整数の演算はアルファベットの演算子な…

今日は制約の続き、let 式からです。 let 式、let 制約 let x = e | A A の中の x を e で置きかえる。つまりx に e を代入(束縛)して A の中で利用するという感じ 再帰的な定義はできない 内包表記 { x1 : e1, x2 : e2, ... | F } e1, e2, ... の各要素から…

今日は関係演算子の定義域、値域の制限演算子説明からです。 s :> - 値域の制限 r :> s は r から s の要素で終わるタプルのみ集めた集合を返す。 ++ - オーバーライド 和集合と似ているが、 p ++ q は同じアトムで始まるタプルがあると q のタプルで上書き…

今日は関係演算子の説明からです。 -> 矢印積 (直積) p -> q で p のタプルと q のタプルの全ての組み合わせを結合した関係を作る p, q のアリティが 2以上なら結果は多項関係になる . ドット結合 p . q で p, q は一般に少なくともどちらか一方は二項関係か…

今日は 3.4 演算子からです。 定数 - none(空集合), univ(普遍集合), iden(恒等関係 全てのアトムから自分自身へのタプルの集合) 集合演算子 + 集合和 & 集合積 - 集合差 in 部分集合 = 等価 in 演算子と = 演算子は評価結果が真偽になる Alloy には同値性と…

今日は 3.3 スナップショット。 Alloy が関係を可視化するやりかたについての説明でした。 ごにょごにょと Alloy をいじって納得したりしましたが文章に書けるようなことでもないので記録は一休み。

「関係」を使って空間的、時間的構造をモデル化 いわゆる構造体みたいな構造だけじゃなく、時系列の変化も関係を使って表現するところがおもしろい 順序付けを表す関係 next で導入する 関係に関係を含める(高階関係)はできない。タプルの要素は常にアトム …

「論理系」の3つの側面について 論理の記述形式 述語論理 自然言語で「全ての○○が□□ならば〜」というのに似た形式 述語論理形式は内包表記で使うことが多い ナビゲーション形式 関係計算 難しいけど短く書けるのでイディオムとして使えるところがある 同じ意…

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

今日は第2章のまとめです。 やらなかったこと 最初から完全なモデルを書いて解析しなかった(インクリメンタルな構築ができると言いたい？) 複雑な数学や記号を使わなかった(使わなくてすむと言いたい？) 「実行可能なコード」を書く必要がなかった トレース…

今日は「実行トレース」について。 モデルの不都合な状態だけでなく、どのような手順でその状態に到達し得るかというのを解析 fact で traces という制約を追加 first, next というキーワードが出てくる 今朝は割り込みがあってこれでおしまい。明日第2章を…

今日はモデルの階層化のところです。 abstract で Java でいう Interface のように抽象クラスを定義して、 extends でそれを継承したシグネチャを定義できる アドレス帳に Alias と Group を作る Composite パターン 本書には「図 2.8 はモデルの宣言を可視…

今日はアサーションの記述について run コマンドを書くかわりに assert でアサーションを書いてみる assert でチェックしたい条件を記述、check コマンドで検査を実行させる 反例(Counterexample) が見つかるとそれを表示してどこに考慮漏れがあったのか観察…

次は「操作」のモデル化です。ちょっと難しくなってきました。 pred add でアドレスの追加を定義 追加前の Book と追加後の Book という表現のしかた 本書の図と実行結果が違う。Book0 でも関連(矢印)がないだけで Addr と Name が表示されている 制約を追加…

第2章から実際に Alloy を使ってみるようです。 「メールクライアントのアドレス帳の設計」という例題 Alloy の具体的な使い方の説明はないんですね。まあなんとかなりましたけど。 sig - シグネチャ。クラスみたいなものかな。「オブジェクトの集合」らしい…