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

今日は第4章の 4.4 型と型検査からです。

• Alloy における型システムは、解析前のエラー検出と、フィールドのオーバーロードを解消(同じフィールド名がどのシグネチャのものかを解決する)に用いられる
• シグネチャには「基本型」がつけられる
  • A1 が A の拡張シグネチャの場合 A1 の型は A の型の部分型であると言う
  • 部分集合シグネチャの場合そのシグネチャ自体の型はなく親の型がつけられる。親(母集団)がシグネチャの和集合の場合(sig C in A + B {})、その型は親の型の和集合となる(型の和集合! しかし「型とは値の集合」という解釈を考えるとこれは自然なことか)
• 式は「関係型」に属する
  • 「関係型」とは基本型の直積の和集合 (A1 -> B1 -> C1, A2 -> B2 -> C2, ...)
• 型は Alloy のシグネチャと式とほぼ同じもの
• 型エラー
  • 関係のアリティの混在
  • 冗長な式 ex) 空集合になる式、部分式を空集合に置換えても結果が変わらない式、など

関数型プログラミング言語における型システムとはちょっと意味合いが違うみたいですね。