问题标签 [vdm++]

有谁知道如何在 vdm++ 中生成随机数？数学库对我不起作用。

我在 VDM++ ToolBox Academic 中遇到了一个愚蠢的错误。

当我尝试运行一个操作时，它给了我这个错误：

我的构造函数是：

我在这里称它为：

我有这个声明：

和（分组）：

错误指向 的第一个字母Game。

有人能帮我吗？

我在 vdm++ 中实现了一个随机数生成器。但我想种子是来自计算机的时钟时间。有谁知道是否有与 c++ 函数等效的 vdm++ 函数time(NULL)？

谢谢你。

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

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

例如。

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

我正在研究一些逻辑表达式。我想将 2 个表达式合并为一个，但不确定如何。我正在使用VDM Overture Tool。

我正在查看一组 5 个温度。有些超过400，有些低于，等等。

当至少 1 个温度超过 400 时，我的第一个表达式为真：

当 set 中的所有值都超过 400 时，第二个表达式为真：

我现在要表达的意思是至少有一个温度超过 400，但不是全部。

任何想法如何将这两者结合起来？

我正在阅读 VDM++ 语言手册。我的问题是在某些情况下他使用“;” 在语句的末尾和同一语句的某处，他没有使用“；”。

下面是例子

I'm using the Tree definition, that comes with The VDM++ Toolbox v9.0.2 and, when trying to use the function addRoot() (using the interpreter), on the first usage, I always get the error: "Run-Time Error 266: Operation or function is not in scope". If I run the function again, it works. Why does it have this behaviour?

I'm adding the Tree code that comes with VDM++ Toolbox. (Please ignore type and syntax errors, since I've fixed them all and it still won't work)

-- START CODE -- The Tree Class

-- END CODE --

我有一个来自 Derek Andrews 和 Darrel INCE 的 VDM 实用形式方法第 5 章的问题，我不确定如何回答，所以在这里，感谢您的帮助！

如果地图价格与汽车价格相关，则集合BL包含 British Leyland 制造的汽车和Fiat 菲亚特制造的汽车。使用本章和集合章节中描述的地图工具和集合工具写下以下描述。

(d) 价格在 6000 英镑到 7000 英镑之间的菲亚特汽车的数量

这是我目前的想法...

1.获取所有法币的价格，即price(fiat)返回价格图的子集

即{punto -→ 5500, panda -→ 6600}

2.可能在地图上限制价格范围（法币）...

但我不确定这是否合法

我认为这应该相对简单，想知道是否有人知道如何回答这个问题：

定义一个递归函数 seq-min : N+ -> N 返回自然数序列中的最小值。

我在想一些类似的事情......

谢谢你的帮助！

示例 1

示例 2

这些句子中的 <> 是什么意思？