Hello, VDM++

ひらめいた！
前回の２つのサンプルに続き、動作はできるけれど事後条件に合わないサンプルを提示するのです。

-- はじめてのVDM(まちがった陽仕様版)
class はじめてのVDM

operations
public hello: () ==> seq of char
hello() ==
    return "こんにちわ, VDM++"          -- まちがった動作を記述
post
    RESULT = "Hello, VDM++";       -- 事後条件

end はじめてのVDM

文法的には正しいし、実行もできます。
しかし、事後条件の検証を有効にすれば、事後条件と実際の戻り値が異なるので、
「契約が成り立っていない」ことが検出できます。

これこそ、VDMらしいです。
やっと、Hello, VDM++が書けそうです。