VDM++は形式仕様記述言語と呼ばれる言語で、仕様を記述するための言語です。

本記事はVDM++の型の組み合わせによってできる型、合成型(Compound Types)の中でも、集合(Set)と配列(Sequence)の簡単なまとめです。

Overture Toolのサイトで公開されている、VDM-10 Language Manualを参考にしています。

2種類の型

VDM++には、プログラミング言語でいう型が存在しており、大きく分けて基本データ型と合成型で構成されています。以下が簡単な説明です。

合成型(Compound Types)

型(基本型か合成型)の組み合わせによってできる型です。以下の8種類の型があります。

今回は、集合と配列について説明します。

同じ型の順序無し集合を扱う型です。

集合の要素は任意の型で構成できるので、例えば、集合自体を集合にすることもできます。

型名	シンボル	意味	文法
set0	`set`	空の要素を許容する順序無し集合	`set of TYPE`
set1	`set1`	空の要素を許容しない順序無し集合	`set1 of TYPE`

※TYPEは任意の型です。

利用できる演算子

利用できる演算子を以下の表に示します。

以下を定義します。

演算子	名前	型
`e in set s1`	`e`が`s1`のメンバである(Membership)	`A` * `set of A` → `bool`
`e not in set s1`	`e`が`s1`のメンバでない(Not membership)	`A` * `set of A` → `bool`
`s1 union s2`	`s1`と`s2`の和集合を生成する(Union)	`set of A` * `set of A` → `set of A`
`s1 inter s2`	`s1`と`s2`の積集合を生成する(Intersection)	`set of A` * `set of A` → `set of A`
`s1 \ s2`	`s2`にない`s1`の要素の集合を生成する(Difference)	`set of A` * `set of A` → `set of A`
`s1 subset s2`	`s1`のすべての要素が`s2`にも存在する(部分集合)(Subset)	`set of A` * `set of A` → `bool`
`s1 psubset s2`	`s1`のすべての要素が`s2`にも存在し、かつ、`s2 / s1`が空でない(真部分集合)(Proper subset)	`set of A` * `set of A` → `bool`
`s1 = s2`	`s1`と`s2`が等しい(Equality)	`set of A` * `set of A` → `bool`
`s1 <> s2`	`s1`と`s2`が等しくない(Inequality)	`set of A` * `set of A` → `bool`
`card s1`	`s1`の要素数を返す(Cardinality)	`set of A` → `nat`
`dunion ss`	`ss`のすべての要素(set)を結合する(Distributed union)	`set of set of A` → `set of A`
`dinter ss`	`ss`のすべての要素(set)を結合する(Distributed intersection)	`set1 of set of A` → `set of A`
`power s1`	`s1`のべき集合を生成する(Finite power set)	`set of A` → `set of set of A`

ちなみに、ここで言うin setはboolを返しますが、内包表記におけるe in set s1は「s1から値を取り出しeと定義する」という意味になります。なんでそんなことになっているかは謎です...

同じ型の配列を扱う型です。

配列の要素は任意の型で構成できるので、例えば、配列を持つ配列を書くこともできます。

型名	シンボル	意味	文法
seq0	`seq`	空の要素を許容する配列	`seq of TYPE`
seq1	`seq1`	空の要素を許容しない配列	`seq1 of TYPE`

※TYPEは任意の型です。

利用できる演算子

利用できる演算子を以下の表に示します。以下を定義します。

演算子	名前	型
`hd l`	`l`の先頭を取り出す(Head)	`seq1 of A` → `A`
`tl l`	`l`の先頭を取り除いた`seq`を取り出す(Tail)	`seq1 of A` → `seq of A`
`len l`	`l`の要素数を返す(Length)	`seq of A` → `nat`
`elems l`	`l`を`l`の`set`に変換する(Elements)	`seq of A` → `set of A`
`inds l`	`l`のインデックスの`set`を生成する(Indexes)	`seq of A` → `set of nat1`
`reverse l`	`l`の順序を反転した`seq`を生成する(Reverse)	`seq of A` → `seq of A`
`l1 ^ l2`	`l1`に`l2`を結合する(Concatenation)	`(seq of A) * (seq of A)` → `seq of A`
`conc ll`	`ll`のすべての要素(`seq`)を結合する(Distributed concatenation)	`seq of seq of A` → `seq of A`
`l ++ m`	`m`の範囲の`l`を返す(Sequence modiﬁcation)	`seq of A * map nat1 to A` → `seq of A`
`l(i)`	`l`の`i`番目の要素を返す(Sequence application)	`seq of A * nat1` → `A`
`l1 = l2`	`l1`と`l2`が等しい(Equality)	`(seq of A) * (seq of A)` → `bool`
`l1 <> l2`	`l1`と`l2`が等しくない(Inequality)	`(seq of A) * (seq of A)` → `bool`

集合と配列には以下の値を代入できます。

集合は{}で、配列は[]で要素を囲みます。

{e1, e2, ..., en}

要素を具体的に記述する方法です。

例

set_1 = { <France>, <Denmark>, <SouthAfrica>, <SaudiArabia> }
seq_1 = [2, 4, 6, 8, 11]
seq_2 = []

{e | bd1, bd2, ..., bdm & P}

要は、Pythonの内包表記です。

例

set_2 = {x * x | x in set {1, 2, 3, 4} & x mod 2 = 0}

{1, 2, 3, 4}から値を順に取り出し、取り出した値をxと定義する。もし、x mod 2= 0がtrueならば、x * xを新たに作るsetに取り入れる。したがって、set_2 = {4, 16}となる。

という感じです。

近いうちに書きます。