单个有限子集的VDM-SL表示法

Question

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

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

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

说“让S是有限的:S⊂ℕ？”是否足够？

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

Answer 1

根据定义，VDM语言中的所有集合都是有限的，因此我认为没有必要显式指定这一部分。按照这里的定义，http://wiki.overturetool.org/images/c/cb/VDM10_lang_manV2.pdf第3.2.1节

现在，要对作为集合s2子集的类型建模，其中一种方法是对该类型使用不变量。例如"inv t == s1 subset s2“。