2011-12-09 抽象によるソフトウェア設計 第4章 言語 その5 今日は第4章の 4.5 ファクト、述語、関数、アサーションからです。 ファクト(fact) 常に成り立つべき制約 シグネチャの宣言の {} の中に書く制約はシグネチャファクトと呼ばれ fact で後で書くのと同等 シグネチャファクト内でフィールド名を展開したくない時は @ をつける 関数 (fun) 関数は単に式を使いまわすためにまとめたもの。C のマクロに近い 述語 (pred) 制約に名前をつけて引数を受け取れるようにしたもの。通常の意味の関数に似てる 制約を on, off してアサーションを検査したりしたい時は述語に(ファクトは常に成り立つ) 関数も述語も呼び出しは [arg1, arg2, ...] をつけて呼ぶ x.f [y, ...] は f [x, y, ...] と同じ(レシーバ構文) アサーション (assert) モデルから導かれるはずの(そのことを検査したい)制約 関数、述語などを呼べる コマンド run コマンド - 述語(pred)の充足例(具体例)を探索させる check コマンド - アサーション(assert)の反例を探索させる いずれも探索範囲(スコープ。トップレベルシグネチャの要素数)を指定できる。省略時は 3 トップレベルシグネチャの要素数と拡張シグネチャの要素数を別々に指定すると、それ意外の拡張シグネチャの要素数はその差となる(上限なので差にならないような気がするけど、なる) check コマンドは書いてなくても処理系からアサーション(名前つき)を指定して実行できればいいのに