VDM ++での操作の指定

Question

この操作での操作の意味を知りたいと思います。ほとんどの行は、 'getStartPrice（）==（return startPrice）'を意味します。

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

Answer 1

"getStartPrice（）==" ラインは、操作のアクションを定義します。驚くべきことは、操作（または関数）の定義が2行で始まることです。最初の行は "op：nat * nat ==> nat"のような型シグネチャを定義し、2行目は "op（a、b）== ..."のようなパラメータの名前を付けます。オペレーションの本文は、暗黙的でない限り、 "=="の後に続くことができます。