问题标签 [vdm++]

vdm-sl 中的智能停车模型

类型

功能

错误行操作 = ; Actor :: id : Id action : 动作 inv mk_Actor(-, action)== action = ;

操作

错误行：

我试图通过 for all 循环运行包含 Brewage 对象的集合中的每个元素。但是当我尝试这样做时，返回值会变得混乱。

循环功能：

酿造构造：

我得到的错误是在 Scan 函数中，如下所示：

操作返回 void 值。实际：(() | Brewage) 预期：Brewage

当我尝试对序列的前两个元素使用纯操作时，会收到此警告。

代码看起来像这样：

它会导致警告：“纯操作调用可能不是引用透明的”，并且 Overture 在函数下方放置了波浪状的黄线hd。

是什么导致了这个警告，我该怎么办？

假设我有一套，S = { 1, 2, 3, 4 }（内容并不重要）

我可以说forall x in set S & x mod 2 = 0，但这会给我一个布尔答案——里面的所有数字都是偶数吗？如果我想查看集合中x mod 2 = 0为真的所有成员怎么办？

将谓词应用于它的语法是什么？如何过滤奇数、偶数、高于/低于 3.5 的数字等？

我有一套S = { 1, 2, 3, 4, 5 }。

通过对其应用数学运算（例如乘法、幂）来更改集合的内容（或者更确切地说，创建一个新集合）的语法是什么？

我有一套，S = { 1, 2, 3, 4, 5 }.

如果我想用标准逻辑总结它，它只是 ∑S（SO 上没有 MathJax，所以我不能很好地格式化这个）。

什么是 VDM 等价物？我在语言参考的数字/集合部分看不到任何内容。

例如，我想在 VDM++ 中将nat转换为 char 的 seq 。

"X is {value of q}"在下面的代码中，如果 q 是 nat 类型并且 q < 3 ，我希望操作 setValueOfX 返回。

我试过使用^，但出现以下错误：

错误 [207] : '^' 的 Rhs 不是序列类型
行为: nat
exp : ( seq1 of # | [] )

假设我有一个函数返回 type 的两个输入值中的较小者int。我想将前提条件设置为只允许 a 和 b 类型int。

当我省略前置条件并进入print Example.min(12.345, 0.123)解释器时，我得到 0.123 作为回报。

解释器窗口

如何确保该函数只接受 type 的输入int？

假设我想为一个接受类型文件的程序建模pdf。

我应该如何在 VDM++ 中模拟接受pdf文件作为输入？

建议函数 T1(F,x,y) == if x = 0 then 1 else y * F(x-1,y) 的定点解决方案我没有回答使用两个变量的问题，例如 x & y 所以当谈到解决这个问题时，我不知道我什么时候完成，或者我是否完全正确。