要素の帰属関係
VDM++ の set 型には、集合に対する要素の帰属関係を定義できます。数学の世界では、ある要素 e が集合 S に含まれるか否かを、e∈S および e∉S と表現します。これを VDM++ では、次のように表現します。
3 in {3,1,2} = true
整数 3 は、集合の要素に含まれるので、true になります。
3 not in {3,1,2} = false
整数 3 は、集合の要素に「含まれる」ので、false になります。
0 not in {3,1,2} = true
整数 0 は、集合の要素に含まれないので、true になります。
{1,2} in {{1,2},{},{3}} = true
集合 {1,2} は、集合の要素に含まれるので、true になります。このように「集合を要素とする」集合に対しても、要素の帰属関係を判定できます。