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