標準ライブラリの使い方（特に入出力）

ツール利用方法の目次に戻る

本ページの内容はあくまで著者がまとめた「簡単に触ってみる第一歩」（Overture IDE 1.1.0 RC1，VDMTools 8.3.1で確認）ですので，詳細なツール仕様や最新の情報については，各ツールの公式Webサイト・マニュアル等をご確認下さい．

大きな画像は縮小しており，クリックすると大きな画像が表示されます．

ライブラリの取り込み

いずれにおいても，単にライブラリファイルが置かれるだけ（パス設定のようなものがあるわけではない）なので，使わなければ単に削除してもよいですし，そのファイルをコピーして別のプロジェクトで使ってもよいです．ただし下記に述べるように一部のライブラリはツール依存で，ツールごとに仕様が異なる可能性もあります．このため用いるツールが提供している標準ライブラリを用いて下さい．

言語仕様外の機能を用いるライブラリ

仕様記述のための言語である（プログラミング言語ではない）VDM-SL・VDM++においては，OSの機能を使うような記述（例えば入出力）を行うことができません．ただし一部の機能については便宜上，ツール側で標準ライブラリとして用意しています．言語仕様外の機能を用いるライブラリにおいては，VDM-SL・VDM++ファイルにて関数・操作のインターフェースのみを定義しています．このため呼び出しの型チェックなどは通常通り行うことができます．実際にこれらの関数・操作の呼び出しを実行すると，（通常は関数・操作本体の記述がないので実行エラーとなるところ）インタプリタ側で適宜必要な機能を提供します．

IOライブラリ

標準入出力やファイル入出力を行うものです．ライブラリファイルを直接開いていただければインターフェースが確認できますが，人によってはよく使うと思うので簡単に解説します．

文字列の出力

文字列を（標準出力へ）出力するには，下記のインターフェースを持つecho操作を用います．

echo: seq of char ==> bool

この操作は成否がbool値で返るので，FAQ「予期せぬ場所で操作の実行が終わってしまう・「実行されない文」という警告が出る」という問題を引き起こしやすいです．意味のない代入を行って回避して下さい．

VDM-SLの場合，一時変数を使うと下記のようになります．

(
  dcl b : bool;
  b := IO`echo("Hello World");
)

上と同じものを，一時定数（無名）を使って書くと下記のようになります．

def - = IO`echo("Hello World") in skip;

VDM++の場合，インスタンス操作になっているのでインスタンスを生成して使います．例えばdefを用いた場合下記のようになります（newでインスタンスを作成し，バッククオートではなくピリオドでクラス名を参照）．

def - = new IO().echo("Hello World") in skip;

任意の値の出力

任意の値の出力を（標準出力へ）行う場合，下記のインターフェースを持つwriteval関数を用います．

writeval[@p]: @p -> bool

任意の型を引数として受け取れるように，便宜上多相関数として定義されています．呼び出すときは具体的な型を与えます．この関数を使うときも，（細かいことを言うと別の理由ですが）意味のない代入を行うことになります．以下ではdef文を用いる例だけ載せておきます．

Overture IDEでのライブラリにおいて，VDM++版のwriteval関数はstaticメンバとして定義されているので，VDM-SLでもVDM++でも呼び出し方は同じです（モジュール名またはクラス名に続きバッククオートでつなぐ）．

def - = IO`writeval[set of int]({1, 2, 3, 4}) in skip;

一方，VDMToolsのVDM++版IOライブラリにおいては，staticメンバにはなっていないので，インスタンスを生成して使います（newでインスタンスを生成性，ピリオドでつなぐ）．

def - = new IO().writeval[set of int]({1, 2, 3, 4}) in skip;

このあたりの仕様はバージョンが変わると統一される（おそらくOverture IDEの方に）かもしれませんが，利用される際にはライブラリファイルを開き，staticなのかそうでないのか，確認して下さい．

何も考えずprint/println

Overture IDEの方では，上記のように型を明示的に指定するのが面倒なので，どんな型の値でも扱えるprint/printlnという操作を便宜上定義しています（引数の型を任意とする記述を用意したようです）．戻り値もないので，無意味な代入を行う必要もありません．本ページの執筆時点ではOverture IDEのみに用意されています．

print: ? ==> ()

ツール利用方法の目次に戻る