问题标签 [vdm++]

在过去的两周里，我一直在为大学学习课程，我已经完成了 90% 的课程。我决定现在打开 Overture，似乎我所有的项目都损坏了:((((((

http://gyazo.com/8e25549bbca700a22399e736a88a1996

如果有人对我如何从中恢复有任何建议/想法，我将不胜感激。我试过“与 -> 本地历史比较”但没有用。现在有点不高兴：[

我已经在我的电脑上安装了 Debian 7。我通过下载和解压 .zip 文件安装了 Overture 工具。每次我尝试运行 Overture 时，都会收到以下错误消息：

有人知道如何解决这个问题吗？

谢谢！

是否可以将 VDM 数学语法与 Overture 一起使用，还是仅限于 ASCII 语法。

或者，在生成 LaTeX 时，可以将数学语法用于输出吗？

我几乎没有使用过 LaTeX。我尝试在 TeX 文件中获取输出 '.tex' 并用 '\forall' 替换 'forall'，然后重新生成 PDF，但只是在 PDF 中插入了 '\forall'。我厌倦了 '$\forall$' 得到相同的结果。

顺便说一句，VDM 和 Overture 的组合为创建规范创造了一个美妙的环境。

当我在 Overture 中从另一个模块导入一个模块时，一切都非常简单。但是，我不知道如何从另一个项目中导入模块。我要做的是：

• 创建项目 P1
• 在 P1 中创建模块 A
• 创建项目 P2
• 在 P2 中指定 P1 作为参考
• 在 P2 中创建模块 B
• 在模块 B 中导入 A

在模块 B 中，系统将错误标记为“没有像 A 这样的模块”。

我想学习如何结合使用 Modelio 和 Overture 来学习使用 UML 和 VDM 对程序进行建模。关于创建 UML 模型、将其导出到 XMI（uml 扩展）以及导入到 Overture 的整个过程已成功完成。

但是，当我尝试将其导出回 Modelio 时，它会带来“失败：文件内容未被识别为有效模型”。Overture 的教程告诉它可以来回导入/导出；但是，到目前为止，该功能似乎已被破坏。

我可能做错了什么。也许我必须以某种方式设置 Overture 才能让 Modelio 理解其导出的 XMI 文件。我所有的在线搜索解决方案都没有成功。我怎样才能成功地从 Overture 导出/导入到 Modelio？

我正在使用 Modelio 3.4.1 和 Overture 2.3.0。

谢谢你。

我看到一些带有扩展显式函数的有趣行为。

我定义了一个隐式函数

以及相应的显式函数（因为后置条件是可计算的）

isLeap2 返回预期值。然后我定义了一个扩展的隐式函数

这可以按预期工作，除非提供的参数是 100 但不是 400 的倍数。结果是

然后当我输入这个时，我想，怎么样

结果和预期的一样。在这种情况下，“=”和“<=>”有什么区别？在 VDM-10 语言手册（2014 年 11 月发行）的第 3.1.1 节中，声明“当我们处理布尔值时，语义上 <=> 和 = 是等价的”。它们在操作上是否不同？

我有一个递归函数，适用于调用堆栈深度高达 1000 的输入，但对于更大的输入则失败。我将该函数转换为尾递归函数，使其可以达到 1350 左右。

有什么限制，有什么办法可以增加这个限制？

我正在使用纯函数，并希望避免使用操作。我有一个解决方案，可以将问题分解为多个步骤的组合，每个步骤的堆栈深度都较小，但这是相当人为的，因为它的唯一目的是避免问题，而且它更复杂。

考虑两个函数定义

在 Overture 中运行 test2(1000) 给出的自然数集最多为 1000。运行 test1(1000) 给出的自然数集合最多为 255。我知道在显式函数定义中存在显式类型绑定时会出现复杂情况，但在这种情况下它只是默默地给出了错误的答案。似乎当自然数的类型绑定出现在定义中时，范围被限制为 0..255。至少，这似乎是从外面发生的事情。

语言手册的第 8 章指出“请注意，类型绑定只能由 VDM 解释器执行，以防可以静态推断类型是有限的。” 对于何时可以静态推断为有限类型是否有任何规则？

我一直在做一本专注于迭代构建整个应用程序的书的练习。在写完四节课后，我正在写第五节课，这是第四节课的测试。但是，Overture 报告“名称 'BinBuilder()' 不在范围内”错误；BinBuilder 是我成功编写的最后一个类。我无法弄清楚这次我在做什么不同。BinBuilder 不是唯一导致问题的类，另外两个也是。因为我不知道出了什么问题，所以我在这里包含了整个事情的链接。谢谢你。

编辑：它链接了从 Overture 导出的 zip 文件，并包含一个显示错误的屏幕截图。

假设我想将实数四舍五入为自然数，我怎么能在 VDM++ 中做到这一点？MATH 库似乎没有执行此操作的任何函数。

谢谢，里卡多