差集合

VDM++ の set 型には、２つの集合の差集合を定義できます。数学の世界では、２つの集合 A および B の差集合を A−B で表現します。VDM++ では、次のように表現します。

    {1, 2} \ {2, 3}        = {1}

一方の集合から他方の集合を除いた後の要素を列挙した、差集合は {1} になります。
《Note》差集合を求める演算では、交換法則/結合法則は成立しません。たとえば、

    let

        s1 = {1, 2},

        s2 = {2, 3}

    in

        s1 \ s2            = {1}

        s2 \ s1            = {3}

のように引数の順序を変えると、異なる結果が得られ、交換法則は成立しません。

    let

        s1 = {1, 2, 3},

        s2 = {2, 3},

        s3 = {3}

    in

        (s1 \ s2) \ s3        = {1}

        s1 \ (s2 \ s3)        = {1, 3}

のように評価の順序を変えると、異なる結果が得られ、結合法則は成立しません。□