theory - 单个有限子集的 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 子集 s2”。