要旨

1.はじめに
バーチャルマシン(以下，VM)はプログラミング言語の処理系の実装で採用されている実行系アーキテクチャである[1].  VMは仮想的なコンピュータシステムであり，命令セットやメモリモデル,外部リソース,外部入出力などを持つ. VMの命令セットはバイトコードまたは中間コード(以下，IRコード)セットと呼ばれ，メモリモデル，外部リソース,外部入出力と併せて,しばしば特定のプログラミング言語（以下，ゲスト言語）向けに設計される．例えば，Java VM (以下，JVM)はゲスト言語としてJava言語を想定して設計されたIRコードセットを持つ[2].  JVMのIRコードセットはJava言語でのメソッドの種類および呼び出し方法に応じて，invokedynamic，invokeinterface, invokespecial,  invokestatic,  invokevirtualなど,それぞれ個別に特化されたメソッド呼び出しのためのIR命令が定義されている．プログラミング言語に特化しつつコンパクトなIRコードセットを定義することで，プラットフォーム間の移植性の高さと，階層化されたメモリを持つ現代的な計算機アーキテクチャにおける効率的な実行を両立した処理系を実装することができる．同一ソースプログラムを複数プラットフォーム上で動作させる場合, VMを界面として，プラットフォーム依存な部分をVMに集中させ，VM上で動作するIRコード列はプラットフォーム非依存にすることができる．同一仕様のVMを複数プラットフォーム上に実装して，プログラムソースから単一のコンパイラを利用してIRコード列を生成し, IRコード列を複数プラットフォーム上で動作させることができる. VMには利点がある一方で，その開発には高い技量を要するという課題がある．VMの仕様，特にIRコードセットの定義およびレジスタとメモリモデルの設計は,ゲスト言語を効率的に実行する上で重要である．シンプルかつゲスト言語の実行モデルに適合したIRコードセットを定義することで，ゲスト言語の単純なインタプリタよりもコンパクトな処理系を実現することができ，かつ，そのコンパクトさによって階層化されたメモリを持つ現代的な計算機アーキテクチャでの実行効率の改善が期待できる．レジスタおよびメモリモデルについても，高性能なVMを実現するためには，適切な抽象度によりIRコードセットを単純化し，かつ，ゲスト言語でのメモリ使用の特性に適合する，オーバーヘッドの少ないシンプルなメモリモデルを設計する必要がある. VMの仕様には高い厳密性が求められる．VMの利点の1つである移植性の高さは，同一仕様のVMはいずれの実装でも同一の仕様に従って動作することに依拠している．VMの仕様に解釈上の曖昧さがあると，ゲスト言語レベルにおいて，実装ごとに異なった振る舞いをする可能性がある.実行系としてのVMには処理速度と信頼性の高いレベルでの両立が求められる．VMの実装には効率的な実行のために技芸的な技術がしばしば適用され，仕様に対して正しい実装となっているかを確認することは容易ではない．個々のIRコードの実装の正しさを確保するためには，適切な粒度と十分な厳密さを持つIRコードセットの定義が求められる．メモリ管理，外部リソースや外部IOについても同様である．また，IRコードレベルの最適化やIRコードからネイティプコードへのJITコンパイルなどの技術が普及しつつあるが，これらの技術もVM仕様に依拠したものである. ViennaVM[4]は著者らが開発中の，実行可能形式仕様記述言語VDM-SLを実行するためのVMである．Vien- naVMの開発では，VMの仕様はVMの実装の処理速度および信頼性の両方に大きな影響を与えると考え，仕様の品質を向上するためのアプローチとしてVDM-SLによる仕様記述を行なった．本論文では，２節でVDM-SLの簡単な概要を説明し，３節でViennaVMのレジスタに関する特徴を説明し，4節でレジスタへのアクセスおよび演算命令のVDM-SL仕様とC言語での実装を示す．5節で，仕様記述工程および実装工程への影響についてテストを中心に議論し，また，現在の実装での性能を評価する．最後に，6節で全体をまとめるとともに，今後の課題を示す.
2. VDM-SLの概要
本節では，ViennaVMの形式仕様記述言語として採用したVDM-SLについて概要を説明する．VDM-SLはモデル規範型の形式仕様記述言語であり，仕様記述者は対象をモジュールに分解して，各モジュールが持つ機能を内部状態および内部状態に対する操作としてモデル化する[5]. VDM-SLでは，システムをモジュール化し，各モジュールをデータ型，定数，関数，状態空間，操作の5種類の定義によって記述する．各モジュールの外部インターフェイスはexports文によって宣言され，外部モジュールが定義する要素への参照はimports文によって宣言する．各モジュールではデータ型をtypes部で宣言し，定数および関数をそれぞれvalues部およびfunctions部で定義することによって，そのモジュールが扱う概念とその関係を記述する．VDM-SLでは定数および関数は参照透明である. state部では，モジュールが持つ内部状態を定義するために，静的に型付けられた変数のリスト，状態が常に守るべき不変条件および初期状態を宣言する．モジュールが提供する操作をoperations部で定義する．操作はプログラミング言語の手続きに相当し，静的に型付けされている． VDM-SLは実行可能なサプセットを持つ. VDM-SLで記述された仕様は，関数や操作について評価する式や文を陽に記述し，かつ，forallなどの限量子や有限集合の内包表記など，全要素の評価が必要な式について，型ではなく有限集合に束縛することで，インタプリタ等で実行することができる．VDMTools[6]，The Overture tool[7, 8],   ViennaTalk[9]などのVDM-SL開発環境はインタプリタを持ち，ユーザは記述中の仕様をインタプリタ実行することで記述対象が持つ振る舞いや特性を理解することができる．さらに，vdmUnitやViennaUnit[10]などの単体テストフレームワークを利用して，VDM-SL仕様を継続的に単体テストすることが可能である．実際の開発適用事例においても，VDM-SLのオプジェクト指向拡張であるVDM++[11]による仕様記述に対するテストが行われ，仕様記述の品質向上および成果物の信頼性向上に高い成果を上げている[12].
3. ViennaVMの特徴
ViennaVMはVDM-SL仕様を実行することを目的としたVMで，VDM-SL仕様から自動生成されたIRコードを，IoTを含む多様なプラットフォーム上で実行することを想定している．VDM-SL仕様からの実装の自動化として，VDM-SLからC++，Java，Smalltalkなどの多様なホスト言語を対象とするプログラムソース自動生成器が研究され開発されている．プログラムソースの自動生成器は実装工程のコストを劇的に削減する一方，ホスト言語の言語仕様および処理系の更新に追従して保守する必要がある．VDM-SLの実行に必要な機能を持つViennaVMの仕様を厳密に記述し，様々なプラットフォーム上でそのプラットフォームに適したプログラミング言語でViennaVMを実装することで，VDM-SLから単一のIRコード自動生成器によって多様なプラットフォーム上で動作する実装を得ることがViennaVM開発の目標である.図1にViennaVMのモジュール構成を示す．ViennaVMは，ViennaVMが扱うデータフォーマットを定義するDataモジュール，レジスタおよびレジスタに対する読み書きを行うRegisterモジュール，ヒープメモリの管理およびヒープメモリに対する読み書きを行うMemoryモジュール，コードプロックを管理するCodeRecordモジュール，実行コンテキストを管理するActivationRecordモジュール，および，コードプロックからIRコードを読み出し実行するInstructionモジュールから成る．本論文では， ViennaVMのモジュールの中でも特にViennaVMに特徴的な設計となっているRegisterモジュールに岩目し，その特徴を説明する.
3.1.安全で効率的なタグ付けとタグ除去
VDM-SLは静的型付け言語であるが，実行には実行時型情報が必要である．ViennaVMでは，データオプジェクトを64ビットのタグ付きワードによって表現する．具体的には，63ビット符号付き整数，32ビット浮動小数点数，32ビットユニコード文字，および56ビットポインタを64ビットのタグ付きポインタに符号化する.データオプジェクトとしてタグ付きワードを採用するVMの多くは，メモリやレジスタにタグ付きワードを格納し，算術演算などタグを除去しての演算が必要な場合にのみ，演算処理を行う時に一時的にタグを除去したデータを取り出し，演算を行い，結果をタグ付きワードに変換する．この方式では，メモリ上のデータ表現をタグ付きワードに統一することで，タグ付きワードとタグを除去されたデータを混同する危険を減少させ，安全にデータを扱うことができる．一方で，複雑な算術演算を行う時には多くのタグ付けとタグ除去が実行されるという欠点がある.冗長なタグ付けとタグ除去を回避するために，明示的にタグ付けおよびタグ除去を行うIRコードを定義するアプローチもある.  IRコードが明示的にタグ付けおよ演算の例びタグ除去を行う場合には，タグ除去されたデータオプジェクトの正当性はIRコードに依拠することになる．例えば，整数値を持つタグ付きワードをタグ除去し，演算を行った結果をポインタとしてタグ付けすることが可能になると，不正なアドレスへのメモリ書き込みが可能になる. ViennaVMでは，冗長なタグ付けとタグ除去を削減するために，タグ付与とタグ除去をレジスタ内部で処理するよう設計した．レジスタをタグ付きワード，符号付き整数，浮動小数点数，ユニコード文字の４つのフィールドを持つレコードとして，算術演算命令やメモリアクセスなどで利用される時にのみタグの除去およびタグの付与が実行され，その結果がフィールドに格納される．その後，同じレジスタに対する算術命令が実行される時には，フィールドに格納されたタグなしデータオプジェクトを直接読み込んで算術演算が実行される．これによって，冗長なタグ付けの回避と安全なタグ付けおよびタグ除去を両立させている.図2にViennaVMの演算命令における自動的なタグ除去の例を示す. 2つの命令add  r1,  r2およびmul rl, rl, r3によって, r1 ← (r1 + r2) *  r3 を実行するためのタグ除去と算術計算の手順を説明する．従来の，算術命令で常にタグ除去を行い，算術演算の結果にタグ付与を行う場合，各算術命令の前に2つのオペランドに対するタグ除去と，各算術命令後に1回のタグ付与が行われ，合計すると4回のタグ除去と2回のタグ付与が実行される．ViennaVMでの自動的なタグ除去およびタグ付与では，３回のタグ除去で同様な算術結果が得られる.まず左端に初期状態として，３つのレジスタr1, r2, r3に，それぞれ整数3, 4, 5がメモリからロードされた状態を仮定する.ここでまず,命令add  r1,  r2を実行する．この命令は，2つのレジスタr1とr2を加算した結果をr1に格納する．レジスタr1にはタグ付きワードフィールド（oid）のみ格納されているため,まずはタグを除去して整数3を得る。レジスタr2も同様で，タグを除去して整数4を得る．加算した結果である整数7をレジスタr1の整数フィールド（i）に格納する．また，レジスタr2の整数フィールド（i）にもタグを除去した結果である整数4を格納する.次に，命令mul rl，rl，r3を実行する．この命令は，2つのレジスタr1とr3を乗算した結果をr1に格納する．レジスタr1には整数フィールド（i）に7が格納されているため，これをそのまま利用する．レジスタr3にはタグ付きワードフィールド（oid）のみ格納されているため，まずはタグを除去して整数5を得る．乗算した結果である整数35をレジスタr1の整数フィールド（i）に格納し，レジスタr3の整数フィールド（i）にもタグを除去した結果である整数5を格納する.以上の手順で２つの算術演算命令が実行されるが，この中でタグ除去は３回のみ行われる．さらに，この後でレジスタr2やレジスタr3の整数値が必要な算術演算命令を実行する場合には，タグ除去なしで整数値を取り出すことができる。レジスタr1にはタグ付きワードフィールド（oid）に値が格納されていないが，タグ付きワードが必要な命令を実行する時点でタグ付与を行なってタグ付きワードフィールドを得る.  ViennaVMは以上の方法で，タグ付けされたデータに対して安全かつ少ないオーバーヘッドによる演算処理を実現している.
3.2.レジスタ空間
JVMを初めとする多くのVMはスタックマシンであり，手続きへの引数および返値の受け渡しはスタックを介して行われる．レジスタの内容を引数または返値としてメモリ上のスタックに書き込むと，第3.1節で説明した自動的にタグ除去されたデータオプジェクトが失われてしまう．また，ViennaVMでは参照カウントによる自動ガーベージコレクション(自動GC)を採用している.コピー GCなど，参照を追跡していくことで参照のないメモリプロックを発見する他の自動GCアルゴリズムに比べて，参照カウントによる自動GCはカウンタの増減という比較的小さなオーバーヘッドで参照のないメモリプロックを自動的に発見し解放することができる．しかし，手続きへの引数や返り値としてポインタ値を保持しているレジスタをメモリ上のスタックに書き込むと，参照カウンタの増減処理が必要になり，メモリ管理のオーバーヘッドを増加させる. ViennaVMでは，メモリ上のスタックを介したデータの受け渡しを避けるために，手続きへの引数および返値の受け渡しはレジスタを介して行う.引数および返値の受け渡し以外に，スタックはレジスタの退避場所としても利用されることがある．一般に多くのVMでは，スタックを使ってレジスタの内容の退避を行う.  ViennaVMではレジスタは４つのフィールドからなるレコードとして定義されるため，レコード全体をスタックに退避させレジスタに復元すると，データトラフィックが大きくなり，性能面で不利である．一方， ViennaVMではヒープメモリ上のメモリプロックにはタグ付きワードのみを格納する．スタックにレジスタ内のデータのうちタグ付きワードを退避復元させる場合には,タグ付けおよびタグ除去の回数が増加し，これも性能面で不利になる. ViennaVMでは，IRコードのオベランドとして指定されるレジスタ番号にオフセットを加えたものを物理的なレジスタ番号として，オフセットを変更することでレジスタの退避および復元を行う．図３にレジスタ番号のオフセットによるレジスタ退避の例を示す. ViennaVMのサプルーチンは，そのコードが利用するレジスタ数を保持する．初期状態として，4つのレジスタを使うサプルーチンをレジスタオフセット値が３で実行しているとする．この時，サプルーチン内ではr1, r2, r3, r4の3つの論理レジスタ名を利用することができ，それらはそれ図3.論理レジスタ番号によるレジスタ退避の例ぞれ実レジスタR4, R5, R6, R7を指す. このサプルーチンから，レジスタを２つ使う別のサプルーチンをcall命令で呼び出す時，引数はr5相当の実レジスタR8, r6相当の実レジスタR9で渡される.  ca11命令はレジスタオフセットを呼び出し側のレジスタ数分増加させる.この例では，+4増加させる．するとレジスタオフセットは７となり，呼び出された側のサプルーチンでは論理レジスタ名r1およびr2はそれぞれ実レジスタr8およびR9を指す。すなわち，第1引数として渡されたデータをレジスタ名r1として受け取る.サプルーチンからの復帰を行うRET命令は，レジスタオフセットを復帰先のレジスタ数分だけ減少させるとともに，復帰元で使用していたレジスタの内容を初期化することで参照カウンタの増減処理を行う.このレジスタ退避の方式の利点は，メモリトラフィックの節約である．例えば手続き呼び出しによってレジスタを10個退避し，後で復元する場合，レジスタレコード単位で退避する方式では640バイトのメモリ間データ転送が必要となる．タグ付きワードのみを退避する場合には，160バイトのメモリ問データ転送と，最大10回のタグ付けと最大10回のタグ除去が必要となる．ViennaVMが採用するレジスタオフセットの場合，オフセット時のホスト言語での整数型の加減算のみでレジスタの退避および復元が可能である. ViennaVMは実レジスタ番号および論理レジスタ番号ともに16ビットのレジスタ空間を持つ．Dalvik VM[3]をはじめとする広いレジスタ空間を持つレジスタマシン方式のVMでは，豊富なレジスタ数を生かしてサプルーチン呼び出しのインライン展開をより深く行うような最適化を可能にしている.  ViennaVMでは，レジスタ番号をオフセットすることで，インライン展開をしなくても豊富なレジスタ数を有効に利用することができる.
4. ViennaVMの仕様と実装
本節では，ViennaVMの仕様と実装について，3.1節および3.2節で説明したレジスタへのデータの読み書きおよび論理レジスタ番号に関するVDM-SL仕様とC言語による実装を説明する.
4.1.レジスタに対するデータの読み書き
3.1節で説明した通り，ViennaVMでは安全かつ効率的なタグ付きワードの扱いのために各レジスタに静的型ごとのフィールドを持たせ，必要に応じてタグ付けおよびタグ除去を行い，その結果を次の使用時に備えて適切なフィールドに格納する．これはViennaVM独自の設計であり，その正確な機能仕様を自然言語および表などの前形式的な表現で定義するだけでは解釈が一意に定まらない危険がある．また，解釈が一意に定まる場合でも，仕様に誤りがある場合に，自然言語などによる記述では誤りの発見が困難であり，しばしば実装後に誤りが発見され，手戻りの原因になり得る．また，ViennaVMでのレジスタの読み書きには，タグ付けおよびタグ除去だけでなく，型変換も伴う場合がある．VDM-SLでは整数型や自然数型が実数型の部分型として定義されている．VDM-SLの言語仕様では実数型の内部表現および精度に関する規定はなく，全ての整数値は実数型の値であり，１．０と１は同じ値を意味する．例えば，式１ = １.０はtrueである．そこで，ViennaVMでは，整数値が格納されたレジスタから浮動小数点数を読み出す時に，読み出し処理の中で整数値から浮動小数点数に変換した値が得られるものとした．本節ではそれがVDM-SLによってどのように定義されているのかを説明する.図4にViennaVM内部でのデータ型定義の一部を抜粋する.  OID型がタグ付き64ビットワード,  Int型は63ビット符号付き整数，Float型は32ビット浮動小数点数，Char型は32ビットユニコード，Pointer型は56ビットポインタとして定義されている．具体的な定義としては，タグ付きワード型OIDや整数型Intがそれぞれ自然数型および整数型に不変条件を与えることによって定義している．また，浮動小数点数型Floatをレコード型で定義している.図５にRegisterモジュールでのレジスタの定義を示す.レコード型Regが, oid, i, f, cの4つのフィールドから構成されるレコード型として定義されている.それぞれのフィールドには，図４で定義されたOID型, Int型, Float型, Char型が静的につけられている.また，レジスタ番号を表す型Registerが自然数としてRegisterモジュールで定義されている.レジスタにデータを書き込む時には，まずは論理レジスタ番号から実レジスタ番号を求め，該当するレジスタの書き込みデータの型に対応するフィールドに書き込み，それ以外のフィールドを無効値に設定する．例として，レジスタに整数値を書き込む操作write_intの仕様を図6に示す。5行目はレジスタオフセットで論理レジスタ番号をオフセットして実レジスタ番号rを求めている．8-9行目は参照カウントによるメモリ管理に関する記述であり，書き込み前のレジスタがポインタであった場合に，書き込みによりその参照が失われるためメモリプロックの参照カウントを減らす.  10行目以降で，iフィールドに整数値を，それ以外のフィールドには無効傾を書き込む.レジスタからデータを読み出す時には，まず対応するフィールドの値が無効値でなければその値を返す．無効値であれば，互換性のある型のフィールドから型変換をしてフィールドに書き込んだ上で，読み出し値とする.例として，レジスタから整数値を読み出す操作read_intの仕様を，関連する2つの操作とともに図7に示す.操作basic_read_intは，指定されたレジスタのｉフィールドに値が格納されていたらそれを返し,さもなくぼoidフィールド（タグ付きワード）に格納された値を整数型に型変換した結果をｉフィールドに書き込んだ上で，それを返す．操作basic_read_floatは同様のことを£フィールドに対して行う.前述のように，VDM-SLでは，整数型intおよび自然数型natおよびnat1は実数型rea1の部分型であり,例えば１.０は実数であるだけでなく整数型の値でもある.つまり,式１ = １.０はtrueである.そこでViennaVMでは，浮動小数点数が格納されたレジスタからも，それが整数でもある場合には整数値として読み出し可能とした.整数basic read int操作は，指定されたレジスタからbasic_read_int操作で整数値を読み出し，もし結
図8. idiv命令の仕様
果が未定義値であった場合には，basic_read_float操作で浮動小数点数値を読み出し，もし結果が未定義値でなく，かつ，整数値であったら，Int型に型変換した結果をｉフィールドに書き込んだ上で，それを返す.上記の浮動小数点数から整数への型変換は，ViennaVMがVDM-SLに特化したVMであることから有用であって，浮動小数点数1.0と整数1が異なる数値として扱われる他の多くのプログラミング言語では不要である. VDM-SLで仕様を記述することで，上記のような複雑な内容を曖昧さなく厳密に記述することができる. write_intおよびread_int操作を使ったIRコードの仕様の例として，図8にidiv命令の仕様を示す.第２オベランドおよび第３オベランドとして指定されたレジスタからRegisterモジュールのread int操作で整数値をそれぞれ読み出し，両方のレジスタから正常に整数値が読み出せた場合に整数除算の結果を第１オペランドとして指定されたレジスタに書き込む.  idiv命令のC言語での実装を図9に示す.図8のVDM-SL仕様に忠実な実装であることがわかる.
5.議論
本節では，VMの開発にVDM-SLを導入したことの影響を議論する．VMに要求される品質項目で特に重視されるものとして，信頼性と性能に着目し， 5.1節でテストやデバッグについて，5.2で性能面について論じる． void idiv ( Register dst , Register srcl , Register src2) { if  ( d s t  &&  s r c l  &&  s r c 2 )  { Int intl = read_int(srcl); Int int2 = read_int(src2); if (intl != invalidIntValue && int2 != invalidIntValue) { write "int ( dst , int l / int 2 ); return ; → err("idiv : _operands_not_integer"); } else {
 } }図9. idiv命令のC言語での実装
5.1.テストおよびデバッグ
ViennaVMのVDM-SL仕様で定義された関数および操作は，ユニットテストフレームワークviennaUnit [4]を使ってテストされた.図10に，Registerモジュールに対応するテストモジュールRegisterTestの抜粋を示す.  ViennaVMの各モジュールに対応してテストモジュールを記述し，仕様を修正する度に自動的に全テストモジュールを実行した．また，VDM-SLで記述されたテストモジュールはC言語に移植され，それをC言語での実装に対する単体テストとして利用した．表1にVDM-SL仕様およびC言語での実装およびテストモジュールの行数およびテストケース数をまとめた. ViennaVMの開発では，VDM-SL向けユニットテストフレームワークViennaUnitを利用した．ViennaUnitは,仕様を編集し保存する度に，IDEがバックグラウンドタスクとして全てのテストケースを実行し，テストが失敗した場合にのみデスクトップ上に通知を表示する機能を提供している．VDM-SL仕様を記述したファイルへの編集が保存されると，ViennaUnitはモジュール名がTestで終わるモジュールをテストモジュールと見なし，テストモジュール内に定義された操作のうち操作名がtestで始まる操作をテストケースと見做して実行する．この機能を利用することで，仕様記述者が明示的にユニットテストを実行するよりも，仕様記述者の負担を増やすことなく高頻度でテストを実行し，仕様の誤りを早期のうちに発見することができた．また，デバッグのための仕様修正に対しても高い頻度でテストが自動的に実行されたため，修正によるリグレッションを早期発見し，再修正することができた. ViennaUnitは，表明検査のための操作を2つ提供している. assert操作は，引数を２つ取り，第１引数がtrueであるかどうかを確認し，trueでない場合に第2引数をエラーメッセージとしてテスト失敗とする. assertEquals操作は，引数を３つ取り，第１引数と第２引数が等しいかどうかを確認し，等しくない場合に第３引数をエラーメッセージとしてテスト失敗とする.テストケースでは上記２つの表明検査を使って，テスト対象の動作を確認する. ViennaVMでの開発では，仕様の誤りの多くはデータ型に付与された不変条件に対する違反として検出された．テストケース内でのassert操作およびassertEquals操作はテスト対象の動作結果に対してのみ検査するのに対して，データ型に付与された不変条件はテスト対象となる動作の中間状態も含め継続的に検査が行われる。多くのテストケースでは，テストケースに直接記述された表明検査よりも，多くの種類のデータ型不変条件が，多くの回数で，テストケースの表明検査よりも先に検査されることが，データ型不変条件が仕様の誤りの発見に有効であった理由と考えられる. C言語での実装のユニットテストは，VDM-SLによるテストモジュールをC言語に移植することで実装した.図11にレジスタへのデータアクセスのテストの一部を

static Int intl = 0x1234;
static int testWriteBoxedIntAndUbox() { write oid (1, int2oid(int1)); assert Equals ( read_int (1), int l , " i n t −> i n t " ) ; assertEquals ( read_float (1), ( Float )( real2float (( float ) intl )) , "int —> float ") ; assert Equals ( read_char (1), invalidCharValue , "int—char"); assert Equals ( read_pointer(l), invalidPointerValue , "int —>pointer"); return 0; }図11. RegisterモジュールのC言語でのテストコードの抜粋抜粋する．Ｃ言語での実装に対するテストで発見された誤りの多くは実装上の誤りであった．例えばレジスタヘのアクセスにおいてポインタを使って計算量を節約して発生した誤りが発見された．一方で，一般のプログラミングで発生する境界条件の誤りや場合分けの抜けなどは,現在のところ見つかっていない．仕様に対するテストで計算式やアルゴリズムの誤りが発見され修正されていたためであると考えられる.形式手法を導入した開発では，仕様記述の工数が増加する一方で実装の工数が大幅に短縮されるフロントローディング効果が報告されている．VM開発でもテスト工程で要する工数が仕様記述工程に前倒しされたと考えられる.  VDM-SLの実行可能な仕様は，プロトタイプやリファレンス実装でのプログラムに近いように見えるが,システムが取りうる状態に対する制約条件を記述するモデル規範型の形式仕様記述言語としての言語機能が，機能定義の誤り発見と実装上の詳細の誤り発見を分離し、フロントローディング効果につながったと考えられる.
5.2.性能
一般に，言語処理系のランタイムとしてのVMに対する要求として，性能への優先順位は高い．VMを開発するにあたって，要求される性能が実現可能であるかどうかは，常に重大な関心事である．本節では，ViennaVMの開発にVDM-SLを導入した結果として，ViennaVMのC言語での実装の性能をフィボナッチ数の計算で計測し，それをVDMインタプリタVDMJとPython3と比較した.表２にその計測結果をまとめた．実行環境として，サーバ機やデスクトップPC向けに広く普及しているx64アーキテクチャのCore i5プロセッサと，組み込みなどで広
ARMv7: 1.4GHz (Raspbian Stretch, 32ビット)く普及しているARMv7プロセッサを対象とした．各プロセッサ上で，VDMJ, ViennaVM,ベンチマークとして30番目のフィポナッチ数を計算するのに要する時間をそれぞれの処理系で10回計測し，その平均を求めた．いずれのプロセッサでも，Python 3を上回る性能を示した．ただし，既に長く実用されているPython 3に対して，ViennaVMは開発途上の段階であり，これからコード量が増加すると性能の劣化が起こる可能性がある.
6.まとめ
ViennaVMの開発にVDM-SLを導入し，C言語による実装を行なった．VMの仕様の多くの部分は，VMの動作を記述するための，VMが扱うデータ型の定義や各IRコードの処理内容の操作的な意味を与えることに占められる．VDM-SLを導入することで，VMの仕様を腰味さなく記述し，仕様の誤りの発見と実装の誤りの発見を明確に分離することができた．また，性能面でも広く利用されているプログラミング言語インタプリタと同等の速度を実現できた．これにより，VM開発に対してもVDM-SLの有効性を示すことができた. ViennaVMの開発は継続中であり，VDM-SLの実行可能なサプセット全体に必要な機能を完成させた上で，JITコンパイルやIRコード書き換えによる最適化などを仕様記述し実装する予定である.