ウィーン開発方式

ウィーン開発方式( VDM )は、コンピュータベースのシステム開発のための形式手法として最も古くから確立されているものの 1 つです。1970 年代にIBM ウィーン研究所^[1]で行われた研究に端を発し、形式仕様言語である VDM 仕様言語 (VDM-SL) に基づく一連の手法とツールを含むまでに成長しました。拡張形式として VDM++ ^{[2]があり、}オブジェクト指向システムと並行システムのモデリングをサポートしています。VDM のサポートには、モデルのプロパティのテストと証明、検証済みの VDM モデルからのプログラム コードの生成など、モデルを分析するための商用および学術的なツールが含まれています。VDM とそのツールは産業界で利用されてきた歴史があり、形式主義に関する研究が進むにつれて、クリティカル システム、コンパイラ、並行システムのエンジニアリングや、コンピュータ サイエンスのロジックに顕著な貢献がもたらされています。

VDM-SL では、プログラミング言語で実現できるよりも高い抽象レベルでコンピューティング システムをモデル化できるため、システム開発の初期段階で設計を分析し、欠陥を含む主要な機能を特定できます。検証されたモデルは、改良プロセスを通じて詳細なシステム設計に変換できます。この言語には形式的なセマンティクスがあり、モデルのプロパティを高いレベルで証明できます。また、実行可能なサブセットも用意されているため、モデルをテストで分析したり、グラフィカル ユーザー インターフェイスで実行したりできるため、モデリング言語自体に精通していない専門家でもモデルを評価できます。

VDM-SLの起源はウィーンのIBM研究所にあり、最初のバージョンの言語はウィーン定義言語（VDL）と呼ばれていました。[ ^{3] VDLは基本的に}操作的意味論の記述に使用され、表示的意味論を提供するVDM-Meta-IVとは対照的でした^[4]

「1972 年の終わりごろ、ウィーン グループは再び、言語定義からコンパイラを体系的に開発するという問題に目を向けました。採用された全体的なアプローチは、「ウィーン開発方式」と呼ばれています...実際に採用されたメタ言語 (「Meta-IV」) は、BEKIČ 74 で PL/1 の主要部分 (ECMA 74 で示されているように、興味深いことに「抽象インタープリタとして記述された正式な標準文書」) を定義するために使用されています。」^[5]

Meta-IV ^[6]とSchorreのMETA II言語、あるいはその後継言語Tree Metaとの間には関連性はない。これらはコンパイラ・コンパイラシステムであり、正式な問題記述には適していない。

そのため、Meta-IV はPL/Iプログラミング言語の「主要部分を定義するために使用されました」。Meta-IV と VDM-SL を使用して遡及的に記述された、または部分的に記述された他のプログラミング言語には、 BASIC プログラミング言語、FORTRAN、APL プログラミング言語、ALGOL 60、Ada プログラミング言語、およびPascal プログラミング言語があります。Meta-IV は、一般にデンマーク流派、イギリス流派、およびアイルランド流派と呼ばれるいくつかの変種に進化しました。

「英国学派」は、言語定義やコンパイラ設計に特に関連しない VDM の側面に関するCliff Jonesの研究から派生しました(Jones 1980、1990)。豊富な基本型のコレクションから構築されたデータ型を使用して、永続的な^[7]状態をモデル化することに重点を置いています。機能は通常、状態に副作用をもたらす可能性のある操作によって記述され、ほとんどの場合、事前条件と事後条件を使用して暗黙的に指定されます。「デンマーク学派」( Bjørner 他1982) は、明示的な操作仕様をより多く使用する建設的なアプローチを強調する傾向があります。デンマーク学派の研究は、ヨーロッパで初めて検証されたAdaコンパイラにつながりました。

この言語のISO標準は1996 年にリリースされました (ISO、1996)。

VDM-SL および VDM++ の構文とセマンティクスについては、VDMTools 言語マニュアルおよび入手可能なテキストで詳しく説明されています。ISO 標準には、言語のセマンティクスの正式な定義が含まれています。この記事の残りの部分では、ISO 定義の交換 (ASCII) 構文を使用します。一部のテキストでは、より簡潔な数学構文が好まれます。

VDM-SL モデルは、データに対して実行される機能の観点から記述されたシステム記述です。これは、データ タイプと、それらに対して実行される関数または操作の一連の定義で構成されます。

VDM-SL には、次のように数字と文字をモデル化する基本タイプが含まれています。

データ型は、モデル化されたシステムの主なデータを表すために定義されます。各型定義では、新しい型名が導入され、基本型またはすでに導入されている型に基づいて表現されます。たとえば、ログイン管理システムのユーザー識別子をモデル化する型は、次のように定義されます。

種類
ユーザーID = nat

データ型に属する値を操作するために、値に対して演算子が定義されます。したがって、自然数の加算、減算などが提供されるほか、等号や不等号などのブール演算子も提供されます。言語では、表現可能な最大数や最小数、または実数の精度は固定されません。このような制約は、各モデルで必要な場合に、データ型不変条件 (定義された型のすべての要素が遵守する必要がある条件を示すブール式) によって定義されます。たとえば、ユーザー ID が 9999 以下であるという要件は、次のように表現されます ( は<=自然数の「以下」ブール演算子です)。

ユーザーID = nat
不正な uid == uid <= 9999

不変式は任意の複雑な論理式にすることができ、定義された型のメンバーシップは不変式を満たす値のみに制限されるため、VDM-SL の型の正しさはすべての状況で自動的に決定できるわけではありません。

その他の基本型には、文字を表す char があります。場合によっては、型の表現がモデルの目的に関係がなく、複雑さが増すだけです。このような場合、型のメンバーは構造化されていないトークンとして表現できます。トークン型の値は、等価性のみを比較できます。トークン型には他の演算子は定義されていません。特定の名前付き値が必要な場合は、引用型として導入されます。各引用型は、型自体と同じ名前の名前付き値 1 つで構成されます。引用型 (引用リテラルと呼ばれる) の値は、等価性のみを比較できます。

たとえば、交通信号コントローラをモデル化する場合、交通信号の色を表す値を引用符の型として定義すると便利な場合があります。

<赤>、<オレンジ>、<オレンジ点滅>、<緑>

基本型だけでは価値が限られています。新しい、より構造化されたデータ型は、型コンストラクタを使用して構築されます。

最も基本的な型コンストラクタは、2 つの定義済み型の結合を形成します。型には(A|B)、型 A のすべての要素と型 のすべての要素が含まれますB。交通信号コントローラの例では、交通信号の色をモデル化する型は次のように定義できます。

信号色 =   <赤> | <オレンジ> | <点滅オレンジ> | <緑>

VDM-SL の列挙型は、上記のように引用型の結合として定義されます。

VDM-SLでは直積型も定義できます。型は(A1*…*An)すべての値の組から構成される型で、最初の要素は型からA1、2番目の要素は型からA2、というように続きます。複合型またはレコード型は、フィールドのラベルが付いた直積です。型

T :: f1:A1
     f2:A2
     ...
     fn:An

は、 というラベルの付いたフィールドを持つ直積ですf1,…,fn。 型の要素はT、 と書かれたコンストラクタによってその構成要素から構成できますmk_T。逆に、 型の要素が与えられた場合T、フィールド名を使用して名前付きコンポーネントを選択できます。たとえば、型

日付 :: day:nat1
        月:nat1
        年:nat
inv mk_Date(d,m,y) == d<=31 かつ m<=12

は単純な日付型をモデル化します。値はmk_Date(1,4,2001)2001 年 4 月 1 日に対応します。日付が与えられるとd、式はd.month月を表す自然数になります。必要に応じて、月ごとの日数や閏年に関する制限を不変式に組み込むことができます。これらを組み合わせると、

mk_Date(1,4,2001).月 = 4

コレクション型は値のグループをモデル化します。セットは、値間の重複が抑制される有限の順序なしコレクションです。シーケンスは、重複が発生する可能性がある有限の順序付きコレクション (リスト) であり、マッピングは 2 つの値セット間の有限の対応を表します。

集合型コンストラクタ（set of TはT定義済み型）は、型 から抽出されたすべての有限値集合からなる型 を構築しますT。たとえば、型定義

UGroup  = UserIdの セット  

UGroupすべての有限の値の集合から構成される型を定義しますUserId。集合の和集合、積集合を構築したり、適切な部分集合関係や厳密でない部分集合関係を決定したりするために、集合に対してさまざまな演算子が定義されています。

有限シーケンス型コンストラクタ（は定義済み型seq of Tとして記述T）は、型 から抽出されたすべての有限値のリストで構成される型 を構築しますT。たとえば、型定義

文字列 =文字
の シーケンス  

すべて有限の文字列で構成される型を定義しますString。連結、要素やサブシーケンスの選択などを構築するために、シーケンスに対してさまざまな演算子が定義されています。これらの演算子の多くは、特定のアプリケーションに対して定義されていないという意味で部分的です。たとえば、3 つの要素のみを含むシーケンスの 5 番目の要素を選択することは未定義です。

シーケンス内の項目の順序と繰り返しは重要であるため、 は[a, b]と等しくなく [b, a]、 は[a]と等しくありません[a, a]。

有限マッピングは、ドメインと範囲の2つのセット間の対応であり、ドメインは範囲の要素をインデックスします。したがって、有限関数に似ています。VDM-SLのマッピング型コンストラクタ（とが定義済み型map T1 to T2として記述されます）は、値のセットから値のセットへのすべての有限マッピングで構成される型を構築します。たとえば、型定義 T1T2T1T2

誕生日 =文字列を日付に マップする   

Birthdays文字列を にマッピングする型を定義しますDate。また、マッピングへのインデックス付け、マッピングのマージ、サブマッピングの上書きと抽出を行うための演算子がマッピング上で定義されます。

VDM-SL と VDM++ 表記法の主な違いは、構造化の扱い方です。VDM-SL には従来のモジュール拡張がありますが、VDM++ にはクラスと継承による従来のオブジェクト指向構造化メカニズムがあります。

VDM-SL の ISO 規格には、さまざまな構造化原則が記載された参考付録があります。これらはすべて、モジュールを使用した従来の情報隠蔽原則に従っており、次のように説明できます。

• モジュールの命名: 各モジュールは、構文的にはキーワードで始まり、moduleその後にモジュール名が続きます。モジュールの最後には、キーワードendが記述され、その後に再びモジュール名が記述されます。
• インポート: 他のモジュールからエクスポートされた定義をインポートすることができます。これは、キーワードで始まり、さまざまなモジュールからの一連のインポートが続くインポート セクションで行われます。これらの各モジュール インポートは、キーワードで始まり、その後にモジュールの名前とモジュール シグネチャが続きます。モジュール シグネチャは、そのモジュールからエクスポートされたすべての定義のインポートを示すキーワードにすることも、一連のインポート シグネチャにすることもできます。インポート シグネチャは、型、値、関数、および操作に固有のものであり、それぞれ対応するキーワードで始まります。さらに、これらのインポート シグネチャは、アクセスする必要がある構成要素に名前を付けます。さらに、オプションの型情報が存在する場合があり、最後に、インポート時に各構成要素の名前を変更することもできます。型の場合、特定の型の内部構造にアクセスするには、キーワードも使用する必要があります。importsfromallstruct
• エクスポート: 他のモジュールにアクセスさせたいモジュールの定義は、キーワードとexportsそれに続くエクスポート モジュール シグネチャを使用してエクスポートされます。エクスポート モジュール シグネチャは、キーワードのみで構成することもall、エクスポート シグネチャのシーケンスとして構成することもできます。このようなエクスポート シグネチャは、型、値、関数、および操作に固有のものであり、それぞれ対応するキーワードで始まります。型の内部構造をエクスポートする場合は、キーワードをstruct使用する必要があります。
• より特殊な機能: VDM-SL ツールの以前のバージョンでは、パラメータ化されたモジュールとそのようなモジュールのインスタンス化もサポートされていました。ただし、これらの機能は産業用アプリケーションではほとんど使用されておらず、これらの機能にはツールの課題が多数あったため、2000 年頃に VDMTools から削除されました。

VDM++ では、クラスと多重継承を使用して構造化が行われます。主要な概念は次のとおりです。

• クラス: 各クラスは、構文的にはキーワードで始まり、classその後にクラス名が続きます。クラスの最後には、キーワードendが記述され、その後に再びクラス名が続きます。
• 継承: クラスが他のクラスから構造を継承する場合、クラス見出しのクラス名の後にキーワードを続け、is subclass ofその後にスーパークラスの名前のコンマ区切りリストを続けることができます。
• アクセス修飾子: VDM++ における情報の隠蔽は、アクセス修飾子を使用するほとんどのオブジェクト指向言語と同じ方法で行われます。VDM++ では、定義はデフォルトでプライベートですが、すべての定義の前で、アクセス修飾子キーワードのいずれかを使用できます: private、publicおよびprotected。

VDM-SL では、関数はモデルで定義されたデータ型に対して定義されます。抽象化をサポートするには、関数がどのように計算されるかを指定せずに、関数が計算する結果を特徴付けることができる必要があります。これを行うための主なメカニズムは、暗黙的な関数定義です。この定義では、結果を計算する式の代わりに、入力変数と結果変数に対する論理述語 (事後条件SQRTと呼ばれます) によって結果のプロパティが与えられます。たとえば、自然数の平方根を計算する 関数は、次のように定義されます。

SQRT (x:nat)r:実
ポスト r*r  =  x

ここで、事後条件は結果を計算する方法を定義するのではなくr、結果にどのような特性があると想定できるかを述べています。これは有効な平方根を返す関数を定義していることに注意してください。正の平方根または負の平方根である必要はありません。上記の仕様は、たとえば、4 の負の平方根を返すが、他のすべての有効な入力の正の平方根を返す関数によって満たされます。VDM-SL の関数は決定論的である必要があるため、上記の例の仕様を満たす関数は、同じ入力に対して常に同じ結果を返す必要があることに注意してください。

事後条件を強化することで、より制約された関数仕様が実現されます。たとえば、次の定義では、関数が正の根を返すように制約されています。

SQRT (x:nat)r:実数
ポスト r*r  =  x かつ r >= 0

すべての関数仕様は、入力変数のみに対する論理述語であり、関数の実行時に満たされると想定される制約を記述する前提条件によって制限される場合があります。たとえば、正の実数のみに作用する平方根計算関数は、次のように指定できます。

SQRTP (x:実数)r:実数
前置 x >= 0後置r*r = xかつr >= 0 
     

前提条件と事後条件は、関数を実装するプログラムが満たすべき契約を形成します。前提条件は、関数が事後条件を満たす結果を返すことを保証する前提を記録します。関数が前提条件を満たさない入力で呼び出された場合、結果は未定義になります (実際には、終了も保証されません)。

VDM-SL は、関数型プログラミング言語のように実行可能な関数の定義もサポートしています。明示的な関数定義では、結果は入力に対する式によって定義されます。たとえば、数値リストの平方のリストを生成する関数は、次のように定義できます。

SqList: seq of nat -> seq of nat
 SqList (s) == if s = [] then [] else [( hd s) ** 2 ] ^ SqList ( tl s)
                   

この再帰定義は、入力と結果の型を指定する関数シグネチャと関数本体で構成されます。同じ関数の暗黙的な定義は、次の形式になる場合があります。

SqListImp (s:natのシーケンス)r: nat
のシーケンスpos​​t len r = len sかつ
forall i in set inds s & r(i) = s(i) ** 2                        

明示的な定義は、単純に言えば、暗黙的に指定された関数の実装です。暗黙の指定に対する明示的な関数定義の正確さは、次のように定義できます。

暗黙の指定が与えられた場合:

f(p: T_p )r: T_r
前前-f(p)
後後-f(p, r)
   

明示的な関数:

f:T_p - > T_r  

次の場合に限り、仕様を満たしているといえます:

forall  p in set T_p & pre -f(p) => f(p): T_rかつpost -f(p, f(p))
          

したがって、「f正しい実装である」は「f仕様を満たしている」と解釈する必要があります。

VDM-SL では、関数には永続的なグローバル変数の状態を変更するなどの副作用はありません。これは多くのプログラミング言語で便利な機能であるため、同様の概念が存在します。関数の代わりに、操作を使用して状態変数(グローバルとも呼ばれます) を変更します。

たとえば、単一の変数で構成される状態がある場合someStateRegister : nat、これを VDM-SL で次のように定義できます。

 someStateRegisterの状態レジスタ: nat
終了  
      

VDM++ では、次のように定義されます。

 インスタンス 変数
   someStateRegister  :  nat

この変数に値をロードする操作は、次のように指定できます。

 LOAD (i:nat)
  ext  wr  someStateRegister:nat
 post someStateRegister = i
    

externals句( ext) は、操作によってアクセスできる状態の部分を指定します。rd読み取り専用アクセスとwr読み取り/書き込みアクセスを示します。

場合によっては、変更される前の状態の値を参照することが重要です。たとえば、変数に値を追加する操作は次のように指定できます。

 ADD (i:nat)
  ext  wr  someStateRegister  :  nat
 post someStateRegister = someStateRegister~ + i
      

ここで、~事後条件内の状態変数のシンボルは、操作の実行前の状態変数の値を示します。

これは暗黙的な関数定義の例です。関数は正の整数のセットから最大の要素を返します。

 max(s:set of nat)r:nat
 pre card s > 0 post r in set s and
 forall r' in set s & r' <= r
       
                    

事後条件は、結果を取得するためのアルゴリズムを定義するのではなく、結果を特徴づけます。セットが空の場合、セット s に r を返す関数はないため、前提条件が必要です。

 multp(i,j:nat)r:nat
前真後r = i*j
  
    

forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))明示的な定義に証明義務を適用するmultp:

 multp(i,j)  ==
 i= 0の場合0 、そうでない場合-even (i)
の場合2 *multp(i/ 2 ,j)
 、そうでない場合j+multp(i- 1 ,j)
   
   
                    

すると証明義務は次のようになります。

  i,  j の場合 :  nat  &  multp(i,j):nat かつ multp(i,  j)  =  i*j

これは次のようにして正しいことが示されます。

1. 再帰が終了することを証明する（これは、各ステップで数値が小さくなることを証明する必要がある）
2. 数学的帰納法

これは、よく知られたデータ構造の状態ベース モデルにおける暗黙的な操作仕様の使用を示す典型的な例です。キューは、型の要素で構成されるシーケンスとしてモデル化されますQelt。表現はQelt無形であるため、トークン型として定義されます。

 種類

 Qelt  = トークン;
 Queue = Qeltのシーケンス;     

 qのキューの状態:キューの終了  
     
 

 操作

 ENQUEUE (e: Qelt )
  ext  wr  q:キュー
post q = q~ ^ [e];      

 DEQUEUE ()e: Qelt
  ext  wr  q:キュー
pre q <> []
 post q~ = [e]^q;        

 IS - EMPTY ()r:bool
  ext  rd  q:キュー
投稿r <= > ( len q = 0 )
       

VDM-SL モデルの非常に単純な例として、顧客の銀行口座の詳細を管理するシステムを考えてみましょう。顧客は顧客番号 ( CustNum ) でモデル化され、口座は口座番号 ( AccNum )でモデル化されます。顧客番号の表現は重要ではないとみなされるため、トークン型でモデル化されます。残高と当座貸越は数値型でモデル化されます。

 AccNum  =  token;
 CustNum = token;
 Balance = int ;
 Overdraft = nat;         

 AccData  :: 所有者 : CustNum残高:残高 
              

 accountMapの銀行の状態: AccNum をAccDataにマップします。overdraftMap : CustNum をOverdraftにマップします。inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
 a.balance >= -overdraftMap(a.owner)
  
        
        
                                                            

操作: NEWC は新しい顧客番号を割り当てます。

 操作
NEWC (od : Overdraft )r : CustNum ext wr overdraftMap : CustNum をOverdraftポストrにマップします。セットdom ~overdraftMap内になく、overdraftMap = ~overdraftMap ++ { r | -> od};
     
        
                

NEWAC は新しい口座番号を割り当て、残高をゼロに設定します。

 NEWAC (cu  : CustNum )r : AccNum ext wr accountMap : AccNumをAccDataにマップrd overdraftMap CustNumをOverdraftにマップpre cu in set dom overdraftMap
 post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r| -> mk_AccData(cu, 0 )}
   
        
          
                    

ACINF は、顧客のすべての口座の残高を、口座番号と残高のマップとして返​​します。

 ACINF (cu  : CustNum )r : AccNum をBalanceにマップしますext rd accountMap : AccNum をAccDataにマップしますpost r = {an | -> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}
      
        
                

さまざまなツールが VDM をサポートしています。

• VDMTools は、デンマークの IFAD 社が開発した以前のバージョンを基に、CSK Systems 社が所有、販売、保守、開発する、VDM および VDM++ 向けの主要な商用ツールでした。マニュアルと実用的なチュートリアルが用意されています。ツールのフル バージョンのすべてのライセンスは無料でご利用いただけます。フル バージョンには、Java および C++ の自動コード生成、ダイナミック リンク ライブラリ、CORBA サポートが含まれています。
• Overture は、もともと Eclipse プラットフォーム上で、その後 Visual Studio Code プラットフォーム上で実行されたすべての VDM 方言 (VDM-SL、VDM++、VDM-RT) に無料で利用できるツール サポートを提供することを目的としたコミュニティ ベースのオープン ソース イニシアチブです。その目的は、産業アプリケーション、研究、教育に役立つ相互運用可能なツールのフレームワークを開発することです。
• vdm-mode は、VDM-SL、VDM++、および VDM-RT を使用して VDM 仕様を記述するための Emacs パッケージのコレクションです。構文の強調表示と編集、オンザフライ構文チェック、テンプレート補完、およびインタープリター サポートをサポートします。
• SpecBox: Adelard のツールは、構文チェック、簡単な意味チェック、および仕様を数学表記で印刷できる LaTeX ファイルの生成を提供します。このツールは無料で利用できますが、これ以上のメンテナンスは行われません。
• LaTeXおよび LaTeX2e マクロは、ISO 標準言語の数学的構文での VDM モデルの表現をサポートするために使用できます。これらは、英国の国立物理学研究所によって開発および保守されています。ドキュメントとマクロはオンラインで入手できます。

VDM はさまざまなアプリケーション ドメインで広く適用されています。最もよく知られているアプリケーションは次のとおりです。

• AdaおよびCHILL コンパイラ: ヨーロッパで最初に検証されたAdaコンパイラは、Dansk Datamatik CenterによってVDMを使用して開発されました。^{[8]同様に、CHILLと}Modula-2のセマンティクスは、VDMを使用して標準で記述されました。
• ConForm: 信頼できるゲートウェイの従来の開発と VDM を使用した開発を比較する British Aerospace での実験。
• Dust-Expert:工業プラントのレイアウトにおける安全性が適切であるかどうかを判断する安全関連のアプリケーションのために英国の Adelard 社が実施したプロジェクト。
• VDMToolsの開発：VDMToolsツールスイートのほとんどのコンポーネントは、VDMを使用して開発されています。この開発は、デンマークのIFADと日本のCSKで行われました。^[9]
• TradeOne: CSK システムズが日本の証券取引所向けに開発した TradeOne バックオフィス システムの主要コンポーネントの一部は、VDM を使用して開発されました。VDM で開発されたコンポーネントと従来の方法で開発されたコードとでは、開発者の生産性と欠陥密度を比較する測定結果があります。
• FeliCa Networks は、携帯電話アプリケーション向け集積回路のオペレーティング システムの開発を報告しました。

VDM の使用は、非常に抽象的なモデルから始まり、これを実装へと展開します。各ステップでは、データの具体化と、操作の分解が行われます。

データの具体化は、抽象的なデータ型をより具体的なデータ構造に開発し、操作の分解は、操作と関数の（抽象的な）暗黙の仕様を、選択したコンピュータ言語で直接実装できるアルゴリズムに開発します。

${\displaystyle {\begin{array}{|rcl|}{\textbf {Specification}}&&{\textbf {Implementation}}\\\hline {\text{Abstract data type}}&\xrightarrow {\text{Data reification}} &{\text{Data structure}}\\{\text{Operations}}&{\xrightarrow[{\text{Operation decomposition}}]{}}&{\text{Algorithms}}\end{array}}}$

データの具体化（段階的な改良）には、仕様で使用されている抽象データ型のより具体的な表現を見つけることが含まれます。実装に到達するまでにいくつかのステップがある場合があります。抽象データ表現の各具体化ステップでは、ABS_REP新しい表現を提案しますNEW_REP。新しい表現が正確であることを示すために、に関連する取得関数が定義されます。つまり、 です。データの具体化の正確さは、 適切性の証明に依存します。つまり、NEW_REPABS_REPretr : NEW_REP -> ABS_REP

 forall  a: ABS_REP  & exists r: NEW_REP & a = retr(r)
      

データ表現が変更されたため、 で動作するように操作と関数を更新する必要があります。新しい操作と関数は、新しい表現でデータ型の不変条件NEW_REPを保持するように示される必要があります。新しい操作と関数が元の仕様にあるものをモデル化していることを証明するためには、次の 2 つの証明義務を果たす必要があります。

• ドメインルール:

 forall  r: NEW_REP & pre - OPA (retr(r)) => pre - OPR (r)
     

• モデリングルール:

 forall  ~r,r: NEW_REP  & pre - OPA (retr(~r))およびpost - OPR (~r,r) => post - OPA (retr(~r,), retr(r))
      

ビジネス セキュリティ システムでは、作業員に ID カードが渡され、工場に出入りするときにカード リーダーに挿入されます。必要な操作:

• INIT()システムを初期化し、ファクトリーが空であると想定します
• ENTER(p : Person)労働者が工場に入ることを記録し、労働者の詳細をIDカードから読み取ります）
• EXIT(p : Person)労働者が工場から退出することを記録する
• IS-PRESENT(p : Person) r : bool指定された労働者が工場内にいるかどうかを確認する

正式には、次のようになります。

 種類

 Person  = トークン;
 Workers = Personのセット;     

 州AWCCSの大統領：労働者の終了  
    
 

 操作

 INIT ()
  ext  wr  pres:ワーカーpost pres = {}; 
    

 ENTER (p  :人)
 ext wr pres :労働者pre pがセット内にありませんpres
 post pres = pres~ union {p};      
            

 EXIT (p  :人)
 ext wr pres :労働者pre p in set pres
 post pres = pres~\{p};      
         

 IS - PRESENT (p  :人) r : bool
 ext rd pres :労働者のポストr <= > p in set pres~
         
       

ほとんどのプログラミング言語にはセットに相当する概念（多くの場合、配列の形式）があるため、仕様の最初のステップは、データをシーケンスで表現することです。同じワーカーが 2 回出現しないようにするため、これらのシーケンスは繰り返しを許可してはなりません。そのため、新しいデータ型に不変式を追加する必要があります。この場合、順序は重要ではないため、 は[a,b]と同じです[b,a]。

ウィーン開発法は、モデルベースのシステムには有効です。ただし、システムが時間ベースの場合には適していません。このような場合には、通信システムの計算(CCS) の方が便利です。

• 形式手法
• 正式な仕様
• ピジンコード
• 述語論理
• 命題計算
• Z仕様言語、VDM-SLの主な代替（比較）

• Bjørner, Dines; Cliff B. Jones (1978)。ウィーン開発方式: メタ言語、コンピュータサイエンス講義ノート 61。ベルリン、ハイデルベルク、ニューヨーク: Springer。ISBN 978-0-387-08766-5。
• O'Regan, Gerard (2006)。ソフトウェア品質への数学的アプローチ。ロンドン: Springer。ISBN 978-1-84628-242-3。
• Cliff B. Jones 編 (1984)。プログラミング言語とその定義 — H. Bekič (1936-1982)。コンピュータサイエンスの講義ノート。第 177 巻。ベルリン、ハイデルベルク、ニューヨーク、東京: Springer-Verlag。doi :10.1007/ BFb0048933。ISBN 978-3-540-13378-0.S2CID 7488558  。
• フィッツジェラルド、JS、ラーセン、PG、「モデリングシステム：ソフトウェアエンジニアリングにおける実用的なツールとテクニック」ケンブリッジ大学出版局、1998年ISBN 0-521-62348-0（日本語版は岩波書店2003年ISBN 4-00-005609-3）^[10]  
• Fitzgerald, JS、Larsen, PG、Mukherjee, P.、Plat, N.、Verhoef, M.、「Validated Designs for Object-directional Systems」、Springer Verlag 2005年、ISBN 1-85233-881-4。サポートWebサイト[1]には、例と無料ツールサポートが含まれています。^[11] 
• Jones, CB、「Systematic Software Development using VDM」、Prentice Hall 1990。ISBN 0-13-880733-7。オンラインでも無料で入手可能: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip 
• Bjørner, D.およびJones, CB、「形式仕様とソフトウェア開発」 、Prentice Hall International、1982 年。ISBN 0-13-880733-7 
• J. Dawes、 『 VDM -SL リファレンス ガイド』、ピットマン、1991 年。ISBN 0-273-03151-1 
• 国際標準化機構、情報技術 - プログラミング言語、その環境およびシステムソフトウェアインターフェース - ウィーン開発方式 - 仕様言語 - パート 1: 基本言語、国際規格 ISO/IEC 13817-1、1996 年 12 月。
• ジョーンズ、CB、「ソフトウェア開発：厳密なアプローチ」、Prentice Hall International、1980年。ISBN 0-13-821884-6 
• Jones, CBおよび Shaw, RC (編)、『体系的ソフトウェア開発のケーススタディ』、Prentice Hall International、1990 年。ISBN 0-13-880733-7 
• Bicarregui, JC、Fitzgerald, JS、Lindsay, PA、Moore, R.、Ritchie, B.、「Proof in VDM: a Practitioner's Guide」。Springer Verlag Formal Approaches to Computing and Information Technology (FACIT)、1994 年。ISBN 3-540-19813-X。 

• VDM および VDM++ に関する情報 (archive.org のアーカイブ コピー)
• ウィーン定義言語 (VDL)
• COMPASSモデリング言語 Archived 19 February 2020 at the Wayback Machine (CML)は、VDM-SLとCSPを組み合わせたもので、 Unifying Theories of Programmingに基づいており、Systems of Systems (SoS)をモデリングするために開発されました。