要素の帰属関係

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 になります。このように「集合を要素とする」集合に対しても、要素の帰属関係を判定できます。