トップエスイーチュートリアル「VDM++による形式仕様記述」

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ってないのかな。