Hello, VDM++

やっぱり言語の性質上、コレでどうだろうか。

-- はじめてのVDM(陰仕様版)
class はじめてのVDM

operations
public hello: () ==> seq of char
hello() ==
    is not yet specified           -- 動作は記述していません
post
    RESULT = "Hello, VDM++";       -- 事後条件

end はじめてのVDM

コレは正しいけれど、動かないwww！
この is not yet specified は私がVDMの中で最も好きな構文です。

こちらは陽仕様。こちらは動きます。

-- はじめてのVDM(陽仕様版)
class はじめてのVDM

operations
public hello: () ==> seq of char
hello() ==
    return "Hello, VDM++"          -- 動作を記述
post
    RESULT = "Hello, VDM++";       -- 事後条件

end はじめてのVDM