c++ - 如何用 VDM++ 语言编写函数

Question

我正在制作 VDM++ 的翻译器。它将 VDM++ 代码转换为 C++。为此，我正在将 VDM++ 映射到 C++。

我想知道如何在 VDM++ 中编写函数？

例如。

float functionX(int var1,float var2){
int x= 10;
float y= 0.3;
return y;
}

我如何在 VDM++ 中编写此代码？

Answer 1

您的示例函数有点不寻常，因为它不使用其参数，但通常 VDM 函数可能如下所示：

func: int * real -> real
func(var1, var2) ==
    var1 + var2;

请注意，该函数是“纯”的，因为它只是一个涉及其参数的表达式（它也可以引用常量并调用其他函数）。有关更多详细信息，我建议您查看语言参考手册。