はじめに
VDM++は形式仕様記述言語と呼ばれる言語で、形式手法を適用するために用います。
VDM++についての詳しい説明はこちら
本記事は型定義に関してのまとめです。
型定義
VDM++はプログラミング言語でいう型が存在しており、大きく分けて基本型と合成型が存在します。
基本型 : 単純に価の集まりをモデリングするもの。
合成型 : 型構成子を他の型（合成型あるいは基本型）に適用することによって得られる型。
--- VDM++によるオブジェクト指向システムの高品質設計と検証より引用
簡単に言うと、基本型は型の最小な定義で、合成型は型（基本型か合成型）の組み合わせによってできる型です。
基本型
大きく分けてブール型、数型、文字型、引用型の4つの型が存在する。
ブール型
いわゆる真理値を扱う型。
| 記号 | 意味 | 値 |
|---|---|---|
| bool | 真理値 | true, false |
数型
いわゆる数字を扱う型。その中でも５種類存在します。
| 記号 | 意味 | 値 |
|---|---|---|
| nat1 | 正の自然数 | 1, 2, 3 など |
| nat | 自然数 | 0, 1, 2 など |
| int | 整数 | -2, -1, 0, 1 など |
| rat | 有理数 | -2.1, -2.0, 1.0, 1.1 など |
| real | 実数 | -3.1, -1/3, 1/2, 2.2 など |
文字型
単一の文字を扱う型。 文字列は文字型の集合(seq of char)です。
| 記号 | 意味 | 値 |
|---|---|---|
| char | 文字 | '1', 'a', '壱' など |
引用型
いわゆる列挙型を扱う型。
| 記号 | 意味 | 値 |
|---|---|---|
| <QuoteLit> | 引用型 | <運転中>, <停止中>, <加速中> など |
注：QuoteLitは任意の文字列
例えば合成型の選択型を利用することで状態を表すことができます。
自動車の状態 = <運転中> | <停止中> | <加速中>
合成型
そのうち書きます。
参考
参考にさせていただきました。ありがとうございました。
おわりに
私はソフトウェア工学に関する研究室に所属する学生です。研究室配属後に形式手法のこと、形式使用記述のこと、VDM++のことを知りました。
VDM++には素晴らしい実績があります。しかし、VDM++の勉強をしようと思っても、なかなかインターネット上では日本語の記事が見つかりません。適用例が多くヒットします。入門者にはとても敷居が高いと思いました。また、VDM++があまり普及していないという要因もあるかと思います。
そこで、入門者向けの記事をネット上で公開することで、VDM++を盛り上げることにつながるのかなあと思い、少しづつ記事にしていこうと考えました。
私自身VDM++の入門者であり、間違いを書くことは多々あるかと思うので、その時はぜひコメント欄にてご教授頂けると幸いです。