演算の型を規定する
演算の型を規定するのに、次のような表現をします。
set of A * set of A -> set of A
A は任意の型を表わします。すると、set of A は、A 型の要素を列挙した集合型を意味します。すると、
set of nat1
は、自然数を表わす nat1 型の要素を列挙した集合型を意味します。たとえば、
{1,2,3}は、この型に適合するのが分かります。set 型に適用できる演算子 union は、２つの値を与えると、１つの値が得られます。たとえば、
{1,2,3} union {3,4} = {1,2,3,4}は、nat1 型の要素を列挙した２つの集合に対して、演算子 union を適用すると、nat1 型の要素を列挙した集合が得られます。すると、この演算の型を規定するには、次のように、
set of nat1 * set of nat1 -> set of nat1
と表現します。
《Note》VDM++ では、整数を表現する３つの型が規定されています。nat1 は自然数を表わします。nat は、nat1 に 0 を加えたものを表わします。int は、nat に負数を加えた「すべての」整数を表わします。□
