やっぱり言語の性質上、コレでどうだろうか。 -- はじめてのVDM(陰仕様版) class はじめてのVDM operations public hello: () ==> seq of char hello() == is not yet specified -- 動作は記述していません post RESULT = "Hello, VDM++"; -- 事後条件 end …