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

今日は第4章の 4.5 ファクト、述語、関数、アサーションからです。

  • ファクト(fact) 常に成り立つべき制約
    • シグネチャの宣言の {} の中に書く制約はシグネチャファクトと呼ばれ fact で後で書くのと同等
      • シグネチャファクト内でフィールド名を展開したくない時は @ をつける
  • 関数 (fun)
    • 関数は単に式を使いまわすためにまとめたもの。C のマクロに近い
  • 述語 (pred)
    • 制約に名前をつけて引数を受け取れるようにしたもの。通常の意味の関数に似てる
    • 制約を on, off してアサーションを検査したりしたい時は述語に(ファクトは常に成り立つ)
  • 関数も述語も呼び出しは [arg1, arg2, ...] をつけて呼ぶ
    • x.f [y, ...] は f [x, y, ...] と同じ(レシーバ構文)
  • アサーション (assert)
    • モデルから導かれるはずの(そのことを検査したい)制約
    • 関数、述語などを呼べる
  • コマンド