http://topse.or.jp/docs/?q=node/16
受けてきた。
VDM++のイントロダクションとして良い勉強になった。
実際使ってみると、陽定義で操作の中身を書くのは簡単。
難しいのは事前条件、事後条件を抜けもれなく書くことだ。
以下は演習課題の一部分
-- multiChoose public multiChoose : set of UserID * nat ==> set of UserID multiChoose(users,num) == ( dcl res : set of UserID := {}; for i = 1 to num do ( let x in set users be st x not in set registered in ( register(x); res := res union {x} ) ); return res ) pre card registered + num <= capacity and card (users \ registered) >= num post registered = registered~ union RESULT and RESULT subset users and RESULT inter registered~ = {} and card RESULT = num;
ただ、こういった事前事後、不変条件の記述と自動検証は、
プログラミング言語に統合されてしまう気がする。
(defn constrained-fn [f x] {:pre [(pos? x)] :post [(= % (* 2 x))]} (f x)) (defn #^{:test (fn [] (assert (= (add1 2) 3)) (assert (= (add1 -1) 0)))} add1 [x] (inc x))
ところで、vdm-mode.elってないのかな。