vdm++ - VDM++での動作仕様

Question

写真の操作の意味を知りたいです。ほとんどの場合、「getStartPrice()== (return startPrice)」という行が意味します。

私もこれは本当に新しいです。

Answer 1

「getStartPrice() ==」行は、操作のアクションを定義します。意外かもしれませんが、操作 (または関数) の定義は 2 行で始まっています。最初の行は、「op: nat * nat ==> nat」のように型シグネチャを定義し、2 行目は、「op(a, b) == ...」のようにパラメーターに名前を付けます。操作の本体は、暗黙的でない限り、「==」の後に続くことができます。