抽象によるソフトウェア設計 第3章 論理系 その3

  • 「関係」を使って空間的、時間的構造をモデル化
    • いわゆる構造体みたいな構造だけじゃなく、時系列の変化も関係を使って表現するところがおもしろい
    • 順序付けを表す関係 next で導入する
  • 関係に関係を含める(高階関係)はできない。タプルの要素は常にアトム
    • 構造は多項関係で表現。RDB みたいな感じ
  • 順序のない関係(Alloy の関係(タプル)は常に順序に意味がある)の表現
    • 順序つき関係 r が対照的であるという制約 r = ~r を追加すればよい
  • 関数的関係 - 各アトムから高々1つのアトムへの対応がある
  • 単射的関係 - 各アトムに高々1つのアトムから対応がある
    • 関数的かつ単射的がいわゆる普通の「単射
  • 関係の最初の列のアトムの集合を「定義域」、最後の列のアトムの集合を「値域」という