抽象によるソフトウェア設計 第4章 言語 その2

今日はシグネチャの宣言について

  • sig A {} - トップレベシグネチャ
  • sig A1 extends A {} で A の部分シグネチャ、拡張シグネチャをを宣言
  • abstract sig A {} とすると A は直接要素を持たずかならずいずれかの拡張シグネチャに属する
  • sig A1 in A {} - 部分集合シグネチャ。部分集合シグネチャどおしが互いに素にならない
    • sig C in A + B {} のように in の後には和集合を書ける(使える演算子は集合和だけ)
  • one sig A {} のように多重度を指定することでそのシグネチャが含む要素の数を指定できる
    • one sig A, B, C extends T {} - A, B, C が列挙型のように宣言できる
  • 多重継承はできるが sig 宣言ではできない。別に fact で制約として書かないといけない
  • フィールドの宣言
    • sig A { f : e } == f in A -> e == all this: A | this.f in e
    • e の前に多重度を書ける
    • 実際には this はキーワード
    • sig A { disj f, g : e } - f, g が同じ範囲式 e を使いつつ互いに素であることを指定
    • sig A { f : e, g : e - f } - フィールドは前に出てくるフィールドに依存した宣言もできる