VDM-SL notation for a single, finite subset

Question

Not sure if this is within the realm of SO but:

Using VDM-SL, I have been looking around for the 'best' way of describing a single, finite subset of ℕ. In my travels I have found several ways that people are conveying this but I wonder which is the most accepted.

I initially thought that F(ℕ) would do but I believe that this is the set of finite subsets of ℕ, rather than a single subset.

Would it be enough to say, "Let S be finite: S ⊂ ℕ?"

Or does such a notation exist?

Answer 1

All sets in VDM language are finite by definition, so I believe there is no need to explicitly specify that part. As defined here http://wiki.overturetool.org/images/c/cb/VDM10_lang_manV2.pdf section 3.2.1

Now, to model a type which is a subset of a set s2 , one of the ways is to use an invariant on that type. such as "inv t == s1 subset s2".