vdm++ - VDM++ 中的操作规范

Question

我想知道图片中的操作是什么意思。最重要的是，'getStartPrice()== (return startPrice)' 是什么意思。

我也很新。

Answer 1

"getStartPrice() ==" 行定义了操作的动作。令人惊讶的是，操作（或函数）定义以两行开头。第一行定义类型签名，如“op: nat * nat ==> nat”，第二行命名参数，如“op(a, b) == ...”。除非它是隐式的，否则操作的主体可以跟在“==”之后。