问题标签 [vdm-sl]

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

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

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

谢谢你的帮助！

不确定这是否在 SO 的范围内，但是：

使用 VDM-SL，我一直在寻找描述 ℕ 的单个有限子集的“最佳”方式。在我的旅行中，我发现了人们传达这一点的几种方式，但我想知道哪种方式最被接受。

我最初认为 F(ℕ) 可以，但我相信这是 ℕ 的有限子集的集合，而不是单个子集。

说“让 S 是有限的：S ⊂ ℕ”就足够了吗？

或者这样的符号是否存在？

在 VDM-SL 中指定隐式函数时，是否可以指定柯里化函数？下面的 test1 和 test2 是显式的 uncurried 和 curried 函数，而 test3 是一个隐式的 uncurried 函数。Overture 都接受了所有内容。test4 是对隐式柯里化函数的尝试，但被 Overture 拒绝。

另外，有没有办法用隐式函数定义来指定它应该是全部的？

我一直在使用 VDM-SL 中的隐式函数定义创建规范，并且效果很好。我现在想使用显式函数定义对规范进行原型设计（此阶段没有操作）。

我可以看到的一种方法是创建一个新模块，该模块模仿隐式规范中定义的函数，但给它们显式定义。

我确信这可以做到，但我怀疑它是否理想。隐式规范和显式规范之间没有联系，尽管其中一个是对另一个的改进。

是否有从隐式转换到显式函数定义的推荐方法。从长远来看，我确实想正式研究这样做，但首先我只是想实现隐式函数规范以演示实际的规范。

我正在尝试使用 VDM-SL Toolbox，但找不到任何教程。如果有人有任何教程，请分享。谢谢

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

功能如下：

最大：N -> N

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

最大（n）=

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

类型之间有什么区别

和

根据语言参考手册*具有更高->的优先级，因此括号无效；它们在语义上是相同的。但是考虑函数定义

每个都使用一种类型，并且定义中使用的模式必须不同才能通过类型检查。这两种类型之间似乎存在差异。这里发生了什么？通过括号，它将参数解释为产品，但没有括号有两个参数，但不知何故，函数的参数类型仍然是产品。这是相当混乱的。有人可以澄清吗？

我正在尝试将 VDM 模型翻译为 Isabelle，但由于某种原因，我所做的不起作用

以下示例是我的模型的 VDM 功能

以下示例代表我尝试翻译它

我得到的错误是：Inner syntax error⌂ Failed to parse prop

vdm-sl 中的智能停车模型

类型

功能

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

操作

错误行：

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

循环功能：

酿造构造：

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

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