Обозначение VDM-SL для одного конечного подмножества
Не уверен, что это в рамках SO, но:
Используя VDM-SL, я искал "лучший" способ описания одного конечного подмножества ℕ. В своих путешествиях я нашел несколько способов, которыми люди передают это, но мне интересно, какой из них является наиболее приемлемым.
Сначала я думал, что F(ℕ) подойдет, но я считаю, что это множество конечных подмножеств ℕ, а не одно подмножество.
Было бы достаточно сказать: "Пусть S конечно: S ⊂ ℕ?"
Или такая запись существует?
1 ответ
Все наборы в языке VDM являются конечными по определению, поэтому я считаю, что нет необходимости явно указывать эту часть. Как определено здесь http://wiki.overturetool.org/images/c/cb/VDM10_lang_manV2.pdf раздел 3.2.1
Теперь, чтобы смоделировать тип, который является подмножеством набора s2, одним из способов является использование инварианта для этого типа. такой как "inv t == s1 subset s2".