问题标签 [vdm++]

所以.. 我正在尝试同时使用 Modelio 和 Overture，但这两个程序对我来说都是新的。

我想先在 Modelio 中制作一个模型，然后将其导出到 Overture。

但它应该以这种方式工作，还是我应该单独制作？

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

我也很新。

我的实例变量遇到了这个问题。它们不会被初始化，我不确定究竟是什么意思。我上的每一节课都是一样的。我发布了以下代码之一：

我希望有人可以帮助我，也许可以解释原因，这样就不会再发生了

问候， 卡米拉

我定义了两种类型：

我还定义了一个测试集：dcl subFeatures : set of string := {"test1", "test2", "test3"}。

我正在尝试通过以下方式生成一组有效配置：

{ elem | elem : config & dom elem = subFeatures and {true} subset rng elem }

当一个配置至少有一个真实的范围值时，它被称为“有效” 。

Overture 正在启动错误Error 4: Cannot get bind values for type config。经过调查，我发现默认情况下 Overture 无法处理无限类型的类型绑定，但事实并非如此，我正在限制地图域。

有更多经验的人可以检查我做错了什么吗？

我将如何定义一个递归函数来找到比 VDM 中的输入数小二的最大幂？

功能如下：

最大：N -> N

到目前为止，我所拥有的是：

最大（n）=

if n=1 then 0
else if n=2 then 1
else ...最大（...）

我对 VDM++ 很陌生，我试图在操作中使用用例来了解它是如何工作的。

我的想法是给操作一个输入，看看它给了我什么作为输出。所以外汇。我的输入可能是：并且我希望输出是偶数。

以下操作失败并给我错误“表达式中的意外令牌”

我正在尝试创建一个简单的“注册”方法。

我遇到的问题是前提条件。如何编写前提条件“用户名是唯一的”？（即user在userswhere中没有user.username = username）

注：users是set一个User

编辑：pre (username not in set users.username)对我来说最有意义，但这甚至无法编译。

我在 VDM++ toolbox lite 上做 VDM++，下面是我的示例代码：

我试图运行代码。成功创建对象，但是当我运行 print getsubj(10,2) 时，它返回错误 Run-Time Error 120: Unknown state component 有人可以帮我提前谢谢你

我正在使用 Java SE 10 的 64 位系统上运行 Widows 7 Professional。我下载了 Overture-2.6.2-win32.win32x86-64.zip 并将其解压缩到 c: 下，然后单击 Overture 应用程序。它开始并要求提供工作区路径。我采用了默认值，但它失败了。日志文件显示了一堆 Java 错误，包括 ClassNotFound。我将 Overture 文件夹移动到 Java 文件夹所在的 Program Files 中。又失败了。Overture 手册表明下载内容包括 Eclipse。我删除了当前的 Eclipse 版本，以防出现问题。还是失败了。我究竟做错了什么？

如何将文本或值打印到控制台以验证我的模型是否正常工作？

我想做这样的事情：

这似乎是可能的，但我只是不知道该怎么做。