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 のサブセットである型をモデル化する方法の 1 つは、その型で不変条件を使用することです。「inv t == s1 サブセット s2」など。