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».