طريقة فيينا للتطوير

طريقة فيينا للتطوير ، وتُعرف اختصارًا بـ VDM، هي واحدة من أقدم الطرق الشكلية المعروفة لتطوير الأنظمة القائمة على الحاسوب. نشأت من أعمال أُنجزت في آي بي إمبعض المعلومات عن هذا العمل، بما في ذلك التقرير الفني TR 25.139 بعنوان "تعريف شكلي لجزء من PL/1"، بتاريخ 20 ديسمبر 1974، أعيد نشره في Jones 1984، الصفحات 107–155. ومن الجدير بالملاحظة قائمة المؤلفين حسب الترتيب: هـ. بيكيتش، د. بيورنر، و. هينهبل، ك. ب. جونز، ب. لوكاس. في سبعينيات القرن العشرين، وتطورت لتشمل مجموعة من التقنيات والأدوات المعتمدة على لغة توصيف شكلية — وهي لغة توصيف طريقة فيينا للتطوير (VDM-SL). ولها صيغة موسعة، وهي طريقة تطوير فيينا ++ (VDM++)،الرمز ++ مستعار من لغة سي++ الموجهة للكائنات والمبنية على لغة C. والتي تدعم نمذجة الأنظمة الكائنية التوجه والمتزامنة. توجد أدوات تجارية وأكاديمية لدعم طريقة فيينا للتطوير لتحليل النماذج، بما في ذلك دعم لاختبار وإثبات خصائص النماذج وتوليد الشيفرة البرمجية من النماذج المعتمدة. كما أن لطريقة فيينا للتطوير تاريخاً في الاستخدام الصناعي، ونشأ عن هذا الأساس الهيكلي المتين عدد متزايد من الأبحاث التي أسهمت بشكل ملحوظ في هندسة الأنظمة الحرجة، والمصارف، والأنظمة المتزامنة، والمنطق ضمن علم الحاسوب.

 الفلسفة 
يمكن نمذجة الأنظمة الحاسوبية باستخدام لغة توصيف طريقة فيينا للتطوير على مستوى عالٍ من التجريد لا يمكن بلوغه باستخدام لغات البرمجة، مما يسمح بتحليل التصاميم وتحديد الخصائص الأساسية، بما في ذلك العيوب، في مرحلة مبكرة من تطوير النظام. ويمكن تحويل النماذج التي تم التحقق منها إلى تصاميم نظام مفصلة عبر عملية تنقيح. وتتميز اللغة بدلالات شكلية، ما يتيح إثبات خصائص النماذج بمستوى عالٍ من الموثوقية. كما تحتوي اللغة على مجموعة قابلة للتنفيذ، بحيث يمكن تحليل النماذج من خلال الاختبار وتنفيذها عبر واجهات المستخدم الرسومية، مما يسمح بتقييمها من قِبل خبراء قد لا يكونون على دراية بلغة النمذجة نفسها.

 التاريخ 
تعود أصول لغة توصيف طريقة فيينا للتطوير إلى مختبر آي بي إم في فيينا، حيث أُطلق على أول نسخة من اللغة اسم لغة تعريف فيينا (VDL).Bjørner&Jones 1978، المقدمة، ص.ix  وقد استُخدمت VDL بشكل أساسي لوصف دلالات التشغيل، بخلاف طريقة فيينا للتطوير – Meta-IV التي قدمت الدلالات التعيينية.ملاحظات تمهيدية بقلم كليف ب. جونز (المحرر) في Bekič 1984، ص.vii
«نحو نهاية عام 1972، عاودت مجموعة فيينا اهتمامها بمشكلة تطوير مترجم من تعريف لغة بطريقة منهجية. وقد أُطلق على النهج العام المتبع اسم "طريقة فيينا للتطوير"... أما اللغة الوصفية التي استُخدمت فعلياً ("ميتا-آي في") فقد استُخدمت لتعريف أجزاء رئيسية من لغة PL/1 (كما وردت في ECMA 74 – وهي وثيقة معايير شكلية مكتوبة كمفسر تجريدي) في BEKIČ 74.»Bjørner&Jones 1978، المقدمة، ص.xi 

لا توجد أي علاقة بين ميتا-آي فيBjørner&Jones 1978، ص.24. ولغة ميتا 2 التي طوّرها شور، أو وريثتها تري ميتا؛ فهذه كانت أنظمة مصرف المصرفات وليست مناسبة لوصف المشكلات بشكل شكلي.

وهكذا، استُخدمت ميتا-آي في "لتعريف أجزاء رئيسية من" لغة البرمجة بي إل/آي. ومن اللغات الأخرى التي وُصفت لاحقاً جزئياً أو كلياً باستخدام Meta-IV وVDM-SL: بيسيك، فورتران، إيه بي إل (لغة برمجة)، ألغول 60، أيدا، وباسكال. وقد تطورت ميتا-آي في إلى عدة صيغ، تُعرف عموماً باسم المدارس الدنماركية، والإنجليزية، والآيرلندية.

تنحدر "المدرسة الإنجليزية" من عمل كليف جونز على جوانب طريقة فيينا للتطوير غير المرتبطة بتعريف اللغة وتصميم المترجمات (جونز 1980، 1990). وتركز هذه المدرسة على نمذجة الحالة الدائمةراجع المقالة  للاطلاع على استخدامها في علوم الحاسوب. باستخدام أنواع بيانات مبنية من مجموعة غنية من الأنواع الأساسية. وتُوصف الوظائف عادة من خلال عمليات قد يكون لها تأثيرات جانبية على الحالة وغالباً ما تُحدد ضمنياً باستخدام شرط مسبق وشرط لاحق. أما "المدرسة الدنماركية" (بيورنر وآخرون 1982) فتميل إلى نهج بنائي مع مواصفات تشغيلية صريحة بدرجة أكبر. وقد أدى العمل في المدرسة الدنماركية إلى إنتاج أول مترجم أيدا مُعتمد أوروبياً.

وقد صدر معيار من المنظمة الدولية للمعايير للغة في عام 1996 (آيزو، 1996).

 ميزات طريقة فيينا للتطوير 
يتم وصف الصياغة والدلالات النحوية لكل من لغة توصيف طريقة فيينا للتطوير وطريقة فيينا للتطوير++ بشكل موسّع في كتيبات لغة أدوات طريقة فيينا للتطوير (VDMTools) وفي النصوص المتوفرة. ويحتوي المعيار الصادر عن المنظمة الدولية للمعايير (آيزو) على تعريف رسمي لدلالات اللغة. في بقية هذه المقالة، تُستخدم صياغة التبادل المحددة في المعيار (أسكي). ويفضّل بعض المؤلفين استخدام تدوين رياضي أكثر إيجازًا.

نموذج لغة توصيف طريقة فيينا للتطوير هو وصف لنظام يُقدَّم من حيث الوظائف المنفذة على البيانات. ويتألف من سلسلة من تعريفات أنواع البيانات والدوال أو العمليات التي تُجرى عليها.

 الأنواع الأساسية: الأنواع العددية، وأنواع الأحرف، والتوكن، والاقتباس 
تتضمن لغة توصيف طريقة فيينا للتطوير أنواعًا أساسية تمثل الأعداد والأحرف كما يلي:

 الأنواع الأساسية bool  نوع البيانات المنطقية   nat  عدد طبيعي (بما في ذلك الصفر)   nat1  الأعداد الطبيعية (باستثناء الصفر)   int  عدد صحيح   rat  عدد كسري  ، حيث  و عددان صحيحان، و ليس  real  عدد حقيقي   char  أحرف   token  توكنات بلا بنية داخلية   <A>  نوع اقتباس يحتوي على القيمة <A>  

يتم تعريف أنواع البيانات لتمثيل البيانات الرئيسية في النظام المُمَثَّل. يقدم كل تعريف نوعًا جديدًا ويمنح تمثيلًا له باستخدام الأنواع الأساسية أو أنواع سبق تعريفها. على سبيل المثال، قد يُعرَّف نوع يمثل معرّفات المستخدمين في نظام إدارة تسجيل الدخول على النحو التالي:
types
UserId = nat

وللتعامل مع القيم التابعة لأنواع البيانات، تُعرَّف عوامل (operators) تعمل على هذه القيم. وبالتالي، يتم توفير عمليات الجمع والطرح للأعداد الطبيعية، وكذلك العمليات المنطقية مثل التساوي وعدم التساوي. لا تحدد اللغة حدًا أقصى أو أدنى للأعداد الممكن تمثيلها أو دقة الأعداد الحقيقية. ويتم تحديد مثل هذه القيود عند الحاجة إليها داخل كل نموذج باستخدام ما يُعرف بثوابت النوع (invariants) — وهي تعبيرات منطقية تشير إلى الشروط التي يجب أن تحققها جميع عناصر النوع المعرف. على سبيل المثال، يُعبَّر عن شرط يقضي بأن معرّفات المستخدمين يجب ألا تتجاوز 9999 على النحو التالي (حيث <= هو عامل "أقل من أو يساوي" على الأعداد الطبيعية):
UserId = nat
inv uid == uid <= 9999

نظرًا لأن الثوابت (invariants) يمكن أن تكون تعبيرات منطقية معقدة بأي درجة، ولأن الانتماء إلى نوع معين يُحدَّد فقط بالقيم التي تحقق الثابت، فإن تحقق صحة النوع (type correctness) في لغة توصيف طريقة فيينا للتطوير ليس قابلًا للحسم تلقائيًا في جميع الحالات.

تشمل الأنواع الأساسية الأخرى char التي تمثل الأحرف. وفي بعض الحالات، لا يكون تمثيل النوع ذا أهمية لغرض النموذج، وقد يؤدي إلى تعقيده. في مثل هذه الحالات، يمكن تمثيل أعضاء النوع باستخدام توكنات بدون بنية داخلية. يمكن مقارنة قيم أنواع التوكن فقط من حيث التساوي – ولا تُعرَّف عليها أي عوامل أخرى. وعندما تكون هناك حاجة إلى قيم مسماة معينة، يتم إدخالها كأنواع اقتباس. يتكوّن كل نوع اقتباس من قيمة واحدة مسماة بنفس اسم النوع. ولا يمكن مقارنة قيم الاقتباس (وتُعرف بالأدبيات المقتبسة) إلا من حيث التساوي.

على سبيل المثال، عند تمثيل وحدة تحكم إشارات المرور، قد يكون من الملائم تعريف القيم التي تمثل ألوان الإشارة كأنواع اقتباس:
<Red>, <Amber>, <FlashingAmber>, <Green>

 مُنشئات الأنواع: الاتحاد، والجداء، والأنواع المركبة 
الأنواع الأساسية وحدها ذات فائدة محدودة. تُبنى أنواع بيانات جديدة وأكثر تنظيمًا باستخدام مُنشئات الأنواع.
 مُنشئات الأنواع الأساسية T1 | T2 | ... | Tn  اتحاد الأنواع T1,...,Tn T1*T2*...*Tn  الجداء الديكارتي للأنواع T1,...,Tn T :: f1:T1 ... fn:Tn   نوع مركب (سجل)

أبسط مُنشئ نوع يُشكّل اتحادًا بين نوعين معرفين مسبقًا. النوع (A|B) يحتوي على جميع عناصر النوع A وجميع عناصر النوع B. في مثال وحدة تحكم إشارة المرور، يمكن تعريف النوع الذي يُمثّل لون الإشارة على النحو التالي:
SignalColour =  <Red> | <Amber> | <FlashingAmber> | <Green>

تُعرّف نوع التعداد في لغة توصيف طريقة فيينا للتطوير كما هو موضح أعلاه بوصفها اتحادات لأنواع اقتباس.

يمكن أيضًا تعريف أنواع الجداء الديكارتي في لغة توصيف طريقة فيينا للتطوير. النوع (A1*…*An) هو نوع يتكوّن من جميع التُرب المرتبة من القيم، حيث العنصر الأول من النوع A1 والثاني من النوع A2 وهكذا. والنوع المركب أو نوع السجل هو جداء ديكارتي مع تسميات للحقول. النوع
T :: f1:A1
     f2:A2
     ...
     fn:An
هو الجداء الديكارتي مع الحقول الموسومة بـf1,…,fn. يمكن تركيب عنصر من النوع T من أجزائه المكونة باستخدام المُنشئ المكتوب على الشكل mk_T. وعلى العكس، عند إعطاء عنصر من النوع T، يمكن استخدام أسماء الحقول لاختيار المكوّن المُسمّى. على سبيل المثال، النوع:
Date :: day:nat1
        month:nat1
        year:nat
inv mk_Date(d,m,y) == d<=31 and m<=12
يمثّل نوع تاريخ بسيط. القيمة mk_Date(1,4,2001) تقابل 1 أبريل 2001. إذا أعطينا تاريخًا d، فإن التعبير d.month يُرجع عددًا طبيعيًا يمثل الشهر. ويمكن دمج قيود على عدد الأيام في كل شهر والسنة الكبيسة في الثابت (invariant) إذا رغبت في ذلك. بدمج هذه:
mk_Date(1,4,2001).month = 4

 المجموعات 
أنواع المجموعات تُنمذج مجموعات من القيم. المجموعات هي مجموعات منتهية غير مرتبة تُزال فيها التكرارات بين القيم. التسلسلات هي مجموعات منتهية مرتبة (قوائم) يمكن أن تحتوي على تكرارات، وتمثل الخرائط علاقات منتهية بين مجموعتين من القيم.

 المجموعات 
مُنشئ نوع المجموعة (يُكتب set of T حيث T هو نوع معرف مسبقًا) يُنشئ نوعًا يتكوّن من جميع المجموعات المنتهية من القيم المأخوذة من النوع T. على سبيل المثال، يُعرّف تعريف النوع التالي:
UGroup = set of UserId
نوع UGroup بوصفه مجموعة منتهية من القيم من نوع UserId. وتوجد العديد من المعاملات المعرفة على المجموعات لبناء اتحادها، وتقاطعها، وتحديد العلاقات بين المجموعات الجزئية الصارمة وغير الصارمة، وغيرها.

 المعاملات الرئيسية على المجموعات (s، s1، s2 مجموعات) {a, b, c}  تعداد مجموعة: مجموعة العناصر a، b، وc {x | x:T & P(x)}  تشكيل مجموعة: مجموعة x من النوع T بحيث تتحقق P(x) {i, ..., j}  مجموعة الأعداد الصحيحة في النطاق من i إلى j e in set s  e عنصر في المجموعة s e not in set s  e ليس عنصرًا في المجموعة s s1 union s2  اتحاد المجموعتين s1 وs2 s1 inter s2  تقاطع المجموعتين s1 وs2 s1 \ s2  الفرق بين المجموعتين s1 وs2 dunion s  الاتحاد الموزع لمجموعة من المجموعات s s1 psubset s2  s1 مجموعة جزئية صارمة من s2 s1 subset s2   s1 مجموعة جزئية غير صارمة من s2 card s  عدد عناصر المجموعة s (القوة التعددية)

 التسلسلات 
مُنشئ نوع التسلسل المنتهي (يُكتب seq of T حيث T هو نوع معرف مسبقًا) يُنشئ نوعًا يتكوّن من جميع القوائم المنتهية من القيم المأخوذة من النوع T. على سبيل المثال، يُعرّف تعريف النوع التالي:
String = seq of char
نوع String بوصفه جميع السلاسل النصية المنتهية من الحروف. توجد عدة معاملات معرفة على التسلسلات لبناء السلاسل، واختيار العناصر، واستخراج تسلسلات فرعية، وغيرها. العديد من هذه المعاملات جزئية، بمعنى أنها غير معرفة لبعض التطبيقات. على سبيل المثال، اختيار العنصر الخامس من تسلسل يحتوي على ثلاثة عناصر فقط غير معرّف.

ترتيب وتكرار العناصر في التسلسل له أهمية، لذا [a, b] لا يساوي [b, a]، و[a] لا يساوي [a, a].

 المعاملات الرئيسية على التسلسلات (s، s1، s2 تسلسلات) [a, b, c]  تعداد تسلسل: تسلسل العناصر a، b، وc [f(x) | x:T & P(x)]  تشكيل تسلسل: تسلسل من التعبيرات f(x) لكل x من النوع العددي T بحيث تتحقق P(x)(يُؤخذ x بترتيب عددي) hd s  الرأس (العنصر الأول) من s tl s  الذيل (باقي التسلسل بعد إزالة الرأس) من s len s  طول التسلسل s elems s  مجموعة عناصر التسلسل s s(i)  العنصر ith من s inds s  مجموعة مؤشرات (فهرسة) التسلسل s s1^s2  تسلسل ناتج عن ربط التسلسلين s1 وs2

 الخرائط 
الخرائط المنتهية هي علاقة بين مجموعتين، النطاق والمدى، حيث يستخدم النطاق لفهرسة عناصر المدى. وهي بذلك تشبه الدوال المنتهية. مُنشئ نوع الخريطة في لغة توصيف طريقة فيينا للتطوير (ويكتب map T1 to T2 حيث T1 وT2 نوعان معرفان مسبقًا) ينشئ نوعًا يتكوّن من جميع الخرائط المنتهية من مجموعة من قيم T1 إلى مجموعة من قيم T2. على سبيل المثال، تعريف النوع التالي:
Birthdays = map String to Date
يُعرّف نوعًا اسمه Birthdays يربط سلاسل الأحرف إلى Date. ويوجد عدد من المعاملات المعرفة على الخرائط مثل الفهرسة داخل الخريطة، دمج الخرائط، والكتابة فوقها واستخراج خرائط فرعية.

المعاملات الرئيسية على الخرائط {a |-> r, b |-> s}  تعداد خريطة: a تقابل r، وb تقابل s {x |-> f(x) | x:T & P(x)}  استيعاب خريطة: x تقابل f(x) لكل x من النوع T بحيث تحقق P(x) dom m  نطاق m rng m  مدى m m(x)  تطبيق m على x m1 munion m2  اتحاد الخريطتين m1 وm2 (يجب أن تكون m1 وm2 متسقة في مناطق التداخل) m1 ++ m2  m1 تُكتب فوقها m2

 التنظيم البنيوي 
الفرق الرئيسي بين الصيغتين لغة توصيف طريقة فيينا للتطوير وVDM++ هو في كيفية التعامل مع التنظيم البنيوي. في لغة توصيف طريقة فيينا للتطوير، هناك توسعة معيارية تقليدية، في حين أن طريقة تطوير فيينا++ تستخدم آلية تنظيم بنيوي موجه للكائنات تشمل الأصناف والوراثة.

 التنظيم البنيوي في لغة توصيف طريقة فيينا للتطوير 
في المعيار الدولي لـ لغة توصيف طريقة فيينا للتطوير، هناك ملحق إرشادي يحتوي على مبادئ مختلفة للتنظيم البنيوي. كلها تتبع مبادئ إخفاء المعلومات التقليدية باستخدام الوحدات، ويمكن شرحها كالتالي:
 تسمية الوحدة: تبدأ كل وحدة برمجيًا بالكلمة المفتاحية module متبوعة باسم الوحدة. في نهاية الوحدة، تُكتب الكلمة end متبوعة مجددًا باسم الوحدة.
 الاستيراد: يمكن استيراد التعريفات التي تم تصديرها من وحدات أخرى. يتم ذلك في قسم الاستيراد الذي يبدأ بالكلمة المفتاحية imports ويتبعها تسلسل من الاستيرادات من وحدات مختلفة. يبدأ كل استيراد باستخدام الكلمة from متبوعة باسم الوحدة وتوقيع الوحدة. يمكن أن يكون توقيع الوحدة ببساطة هو الكلمة all مما يدل على استيراد كل التعريفات المُصدَّرة من تلك الوحدة، أو يمكن أن يكون تسلسلًا من توقيعات الاستيراد. توقيعات الاستيراد تكون خاصة بالأنواع والقيم والدوال والعمليات، وتبدأ كل منها بالكلمة المفتاحية المناسبة. يمكن أن تتضمن توقيعات الاستيراد معلومات نوعية اختيارية، ومن الممكن أيضًا إعادة تسمية كل من البنى عند الاستيراد. للأنواع، يجب أيضًا استخدام الكلمة المفتاحية struct إذا كان هناك رغبة في الوصول إلى البنية الداخلية لنوع معين.
 التصدير: يتم تصدير التعريفات من وحدة بحيث تكون متاحة للوحدات الأخرى باستخدام الكلمة exports متبوعة بتوقيع الوحدة المُصدِّرة. يمكن أن يكون توقيع التصدير ببساطة الكلمة all أو تسلسلًا من توقيعات التصدير. توقيعات التصدير تكون خاصة بالأنواع والقيم والدوال والعمليات، وتبدأ كل منها بالكلمة المفتاحية المناسبة. إذا كان هناك رغبة في تصدير البنية الداخلية لنوع ما، يجب استخدام الكلمة struct.
 خصائص أكثر تقدمًا: في الإصدارات السابقة من أدوات لغة توصيف طريقة فيينا للتطوير، كان هناك دعم للوحدات المُعلَّمة (المُعمّمة) وتطبيقاتها. لكن هذه الخصائص أُزيلت من أدوات طريقة فيينا للتطوير حوالي سنة 2000 لأنها نادرًا ما استُخدمت في التطبيقات الصناعية، كما أنها سببت عددًا كبيرًا من التحديات في أدوات التطوير.

 التنظيم البنيوي في طريقة تطوير فيينا++ 
في طريقة تطوير فيينا++ يتم التنظيم البنيوي باستخدام الأصناف والوراثة المتعددة. المفاهيم الأساسية هي:
 الصنف: يبدأ كل صنف برمجيًا بالكلمة class متبوعة باسم الصنف. في نهاية الصنف، تُكتب الكلمة end متبوعة مجددًا باسم الصنف.
 الوراثة: إذا كان الصنف يرث من أصناف أخرى، يمكن أن يُتبع اسم الصنف في عنوان الصنف بالكلمات is subclass of متبوعة بقائمة مفصولة بفواصل من أسماء الأصناف الأب.
 مُعدّلات الوصول: يتم تنفيذ إخفاء المعلومات في طريقة تطوير فيينا++ بنفس الطريقة في معظم لغات البرمجة كائنية التوجه باستخدام مُعدّلات الوصول. بشكل افتراضي، تكون التعريفات في طريقة تطوير فيينا++ خاصة، ولكن يمكن استخدام واحدة من الكلمات المفتاحية التالية أمام كل تعريف: private، public وprotected.

 نمذجة الوظائف 
 النمذجة الوظيفية 
في لغة لغة توصيف طريقة فيينا للتطوير، تُعرّف الدوال اعتمادًا على أنواع البيانات المعرفة ضمن النموذج. ويتطلب دعم التجريد أن يكون من الممكن وصف النتيجة التي يجب أن تحسبها الدالة دون الحاجة إلى تحديد كيفية حسابها. وتُعد "تعريفات الدوال الضمنية" الآلية الأساسية لتحقيق ذلك، حيث يُستخدم في هذه التعريفات مُحمَّل منطقي على متغيرات الإدخال والنتيجة، يُعرف بـ "شرط ما بعد التنفيذ"، لتحديد خصائص النتيجة.

على سبيل المثال، يمكن تعريف دالة SQRT لحساب الجذر التربيعي لعدد طبيعي كما يلي:
SQRT(x:nat)r:real
post r*r = x
في هذا المثال، لا يوضح شرط ما بعد التنفيذ طريقة حساب النتيجة r، بل يحدد الخصائص التي يُفترض أن تحققها. لاحظ أن هذا يعرّف دالة تُرجع جذرًا تربيعيًا صالحًا، دون اشتراط أن يكون الجذر موجبًا أو سالبًا. على سبيل المثال، يمكن لدالة تُرجع الجذر السالب للعدد 4، والجذر الموجب لبقية القيم، أن تفي بالمواصفة أعلاه. ومع ذلك، يجب أن تكون الدوال في لغة توصيف طريقة فيينا للتطوير "حتمية"، أي أنها يجب أن تُرجع نفس النتيجة دومًا لنفس المُدخل.

يمكن الحصول على مواصفة أكثر تقييدًا للدالة عن طريق تقوية شرط ما بعد التنفيذ. على سبيل المثال، التعريف التالي يُقيّد الدالة بإرجاع الجذر الموجب فقط:
SQRT(x:nat)r:real
post r*r = x and r>=0
ويمكن تقييد كل مواصفة دالة باستخدام "شروط ما قبل التنفيذ" وهي مُحمَّلات منطقية تنطبق فقط على المتغيرات المُدخلة، وتصف القيود التي يُفترض أن تكون محققة عند تنفيذ الدالة. على سبيل المثال، يمكن تحديد دالة لحساب الجذر التربيعي للأعداد الحقيقية الموجبة فقط كما يلي:
SQRTP(x:real)r:real
pre x >=0
post r*r = x and r>=0
يشكل شرطا ما قبل وما بعد التنفيذ "عقدًا" يجب على أي برنامج يدعي تنفيذ الدالة الالتزام به. إذ يُعبّر شرط ما قبل التنفيذ عن الافتراضات التي تضمن تحتها الدالة إرجاع نتيجة تحقق شرط ما بعد التنفيذ. وإذا تم استدعاء دالة على مُدخلات لا تحقق شرط ما قبل التنفيذ، تكون النتيجة غير معرفة (بل وقد لا تنتهي العملية أصلًا).

تدعم لغة توصيف طريقة فيينا للتطوير أيضًا تعريف دوال قابلة للتنفيذ على طريقة لغات البرمجة الوظيفية. في "تعريف الدالة الصريح"، يتم تحديد النتيجة باستخدام تعبير رياضي على المُدخلات. على سبيل المثال، يمكن تعريف دالة تُنتج قائمة من مربعات قائمة من الأعداد كما يلي:
SqList: seq of nat -> seq of nat
SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)
يتكوَّن هذا التعريف التكراري من توقيع للدالة يحدد نوعي المُدخل والنتيجة، وجسم دالة يوضح آلية الحساب. أما تعريف الدالة الضمني نفسه فيمكن أن يأخذ الشكل التالي:
SqListImp(s:seq of nat)r:seq of nat
post len r = len s and
     forall i in set inds s & r(i) = s(i)**2
يمكن اعتبار التعريف الصريح تنفيذًا مباشرًا للدالة المحددة ضمنيًا. وتُحدد صحة التعريف الصريح بالنسبة إلى المواصفة الضمنية كما يلي:

بالنظر إلى المواصفة الضمنية:
f(p:T_p)r:T_r
pre pre-f(p)
post post-f(p, r)
ودالة صريحة:
f:T_p -> T_r
فإننا نقول إنها تحقق المواصفة إذا وفقط إذا:
forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))
وبالتالي، يجب تفسير "الدالة f هي تنفيذ صحيح" على أنها "الدالة f تحقق المواصفة".

 النمذجة القائمة على الحالة 
في لغة توصيف طريقة فيينا للتطوير، لا تملك الدوال تأثيرات جانبية مثل تغيير حالة متغير عمومي دائم. ومع أن هذه القدرة مفيدة في كثير من لغات البرمجة، فإن هناك مفهومًا مشابهًا في VDM-SL؛ إذ تُستخدم "العمليات" لتغيير "متغيرات الحالة" (المعروفة أيضًا بـ "العموميات").

على سبيل المثال، إذا كان لدينا حالة تتكوَّن من متغير واحد someStateRegister : nat، فيمكن تعريف هذه الحالة في لغة توصيف طريقة فيينا للتطوير كما يلي:
state Register of
  someStateRegister : nat
end
أما في VDM++، فسيتم تعريفها كالتالي:
instance variables
  someStateRegister : nat
ويمكن تحديد عملية لتحميل قيمة إلى هذا المتغير كما يلي:
LOAD(i:nat)
ext wr someStateRegister:nat
post someStateRegister = i
تُحدد جملة "الخارجيات" (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
تقوم شرطية ما بعد التنفيذ بتوصيف النتيجة بدلاً من تحديد خوارزمية للحصول عليها. وتُستخدم شرطية ما قبل التنفيذ لأنّه لا يمكن لأي دالة أن تُرجع قيمة r تنتمي إلى s إذا كانت المجموعة فارغة.

 الضرب للأعداد الطبيعية 
 multp(i,j:nat)r:nat
 pre true
 post r = i*j
عند تطبيق التزام الإثبات forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p)) على تعريف صريح للدالة multp:
 multp(i,j) ==
  if i=0
  then 0
  else if is-even(i)
       then 2*multp(i/2,j)
       else j+multp(i-1,j)
فإن التزام الإثبات يصبح:
 forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j
ويمكن إثبات صحة ذلك عبر:
 إثبات أن الاستدعاء التكراري ينتهي (وهذا بدوره يتطلب إثبات أن الأعداد تصبح أصغر في كل خطوة)
 استقراء رياضي

 نوع بيانات مُجرد للطابور 
هذا مثال كلاسيكي يوضّح استخدام المواصفات الضمنية للعمليات في نموذج قائم على الحالة لبنية بيانات معروفة. يُنمذج الطابور كسلسلة مكوّنة من عناصر من النوع Qelt. وتمثيل Qelt ليس مهماً، ولذلك يُعرَّف كنوع رمز.
 types

 Qelt = token;
 Queue = seq of Qelt;

 state TheQueue of
   q : Queue
 end

 operations

 ENQUEUE(e:Qelt)
 ext wr q:Queue
 post q = q~ ^ [e]؛

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

 IS-EMPTY()r:bool
 ext rd q:Queue
 post r <=> (len q = 0)

 مثال نظام مصرفي 
كمثال بسيط جداً على نموذج لغة توصيف طريقة فيينا للتطوير، نأخذ نظاماً يحتفظ بتفاصيل حسابات العملاء المصرفية. يُمثَّل العملاء بأرقام العملاء (CustNum)، وتُمثَّل الحسابات بأرقام الحسابات (AccNum). وتمثيلات أرقام العملاء تُعد غير مهمة ولذلك يُعبَّر عنها كنوع رمز. أما الأرصدة والسُحوبات المكشوفة فتُنمذج بأنواع عددية.
 AccNum = token;
 CustNum = token;
 Balance = int;
 Overdraft = nat;

 AccData :: owner : CustNum
            balance : Balance

 state Bank of
   accountMap : map AccNum to AccData
   overdraftMap : map CustNum to 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 بتخصيص رقم عميل جديد:
 operations
 NEWC(od : Overdraft)r : CustNum
 ext wr overdraftMap : map CustNum to Overdraft
 post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};

تقوم العملية NEWAC بتخصيص رقم حساب جديد وتعيين الرصيد إلى صفر:
 NEWAC(cu : CustNum)r : AccNum
 ext wr accountMap : map AccNum to AccData
     rd overdraftMap map CustNum to 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 : map AccNum to Balance
 ext rd accountMap : map AccNum to AccData
 post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}

 دعم الأدوات 

توجد العديد من الأدوات المختلفة التي تدعم طريقة فيينا للتطوير:
 VDMTools: كانت الأداة التجارية الرائدة لـ طريقة فيينا للتطوير وVDM++، وتمتلكها وتسوّقها وتدعمها وتطوّرها شركة CSK Systems، استناداً إلى نسخ سابقة طوّرتها الشركة الدنماركية IFAD. تتوفر الكتيبات ودليل عملي. جميع التراخيص متاحة مجاناً للنسخة الكاملة من الأداة، والتي تتضمن توليد كود تلقائي لـ Java وC++، ودعم مكتبة الربط الديناميكي ودعم CORBA.
 Overture: مبادرة مفتوحة المصدر يقودها المجتمع، تهدف إلى توفير دعم أدوات مجاني لجميع لهجات طريقة فيينا للتطوير (VDM-SL، VDM++، وVDM-RT)، وكان ذلك في الأصل على منصة Eclipse ثم لاحقاً على منصة Visual Studio Code. الهدف منها تطوير إطار عمل لأدوات قابلة للتشغيل المتبادل مفيدة في التطبيقات الصناعية والبحث والتعليم.
 vdm-mode: مجموعة من حزم Emacs لكتابة مواصفات طريقة فيينا للتطوير باستخدام لغة توصيف طريقة فيينا للتطوير وVDM++ وVDM-RT. تدعم التمييز اللوني والتحرير، والتحقق الفوري من صحة الصياغة، وإكمال القوالب، ودعم المفسر.
 SpecBox: من شركة Adelard، يوفر التحقق من صحة الصياغة، وبعض الفحوصات الدلالية البسيطة، وتوليد ملف LaTeX يتيح طباعة المواصفات بصياغة رياضية. هذه الأداة متاحة مجاناً ولكن لم يعد يتم تطويرها.
 لاتخ وحزم LaTeX2e متاحة لدعم عرض نماذج طريقة فيينا للتطوير باستخدام الصياغة الرياضية للغة المعيار الدولي. تم تطويرها ويتم صيانتها من قبل المختبر الفيزيائي الوطني في المملكة المتحدة. تتوفر الوثائق والحزم على الإنترنت.

 الخبرة الصناعية 
تم تطبيق طريقة فيينا للتطوير على نطاق واسع في مجالات تطبيقية متنوعة. من أشهر هذه التطبيقات:
 مصرفات أيدا وتشيل: تم تطوير أول مُجمّع أدا تم التحقق من صحته في أوروبا بواسطة مركز دانسك داتاماتيك باستخدام طريقة فيينا للتطوير. كما تم وصف الدلالات لتشيل ومودولا-2 في معاييرها باستخدام طريقة فيينا للتطوير.
 كونفورم: تجربة في شركة شركة بريتيش ايروسبيس لمقارنة التطوير التقليدي لبوابة موثوقة مع التطوير باستخدام طريقة فيينا للتطوير.
 دست-إكسبرت: مشروع نفذته أديلارد في المملكة المتحدة لتطبيق متعلق بالسلامة يهدف إلى تحديد ملاءمة السلامة في تخطيط المنشآت الصناعية.
 تطوير أدوات طريقة فيينا: معظم مكونات حزمة أدوات طريقة فيينا تم تطويرها نفسها باستخدام طريقة فيينا للتطوير. وقد جرى هذا التطوير في IFAD في الدنمارك وشركة سي إس كيه القابضة في اليابان.Peter Gorm Larsen, "Ten Years of Historical Development "Bootstrapping" VDMTools" , In Journal of Universal Computer Science, volume 7(8), 2001
 تريد ون: تم تطوير بعض المكونات الرئيسية لنظام تريد ون الخلفي من قبل أنظمة سي إس كي لبورصة طوكيو باستخدام طريقة فيينا للتطوير. وتوجد قياسات مقارنة لإنتاجية المطورين وكثافة العيوب للمكونات المطورة بـ طريقة فيينا للتطوير مقابل الكود المطور بالطريقة التقليدية.
 أبلغت شبكات فيليكا عن تطوير نظام تشغيل لدارة متكاملة لتطبيقات الهاتف المحمول.

 التحسين 
يبدأ استخدام طريقة فيينا للتطوير بنموذج عالي التجريد ثم يُطوّر هذا إلى تنفيذ فعلي. كل خطوة تتضمن تجسيد البيانات ثم تفكيك العمليات.

تجسيد البيانات يحول نوع بيانات مجرد إلى بنية بيانات أكثر تحديدًا، بينما تفكيك العمليات يحول المواصفات الضمنية (المجردة) للعمليات والدوال إلى خوارزميةات قابلة للتنفيذ مباشرة بلغة برمجة مختارة.

 تجسيد البيانات 
تجسيد البيانات (التحسين خطوة بخطوة) ينطوي على إيجاد تمثيل أكثر تحديدًا لأنواع البيانات المجردة المستخدمة في المواصفة. قد تكون هناك عدة خطوات قبل الوصول إلى التنفيذ. كل خطوة تجسيد لتمثيل بيانات مجرد ABS_REP تتطلب اقتراح تمثيل جديد NEW_REP. لإثبات دقة التمثيل الجديد، يتم تعريف دالة استرجاع تربط NEW_REP بـ ABS_REP، أي retr : NEW_REP -> ABS_REP. تعتمد صحة تجسيد البيانات على إثبات الكفاية، أي:
 forall a:ABS_REP & exists r:NEW_REP & a = retr(r)
وبما أن تمثيل البيانات قد تغير، من الضروري تحديث العمليات والدوال لتعمل على NEW_REP. يجب إثبات أن العمليات والدوال الجديدة تحافظ على أي لامتغير (رياضيات) لنوع البيانات على التمثيل الجديد. ولإثبات أن العمليات والدوال الجديدة تحاكي تلك الموجودة في المواصفة الأصلية، يجب الوفاء بواجبين برهانيين:
 قاعدة النطاق (Domain rule):
 forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
 قاعدة النمذجة (Modelling rule):
 forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))

 مثال على تجسيد البيانات 
في نظام أمني صناعي، يُمنح العمال بطاقات هوية؛ تُستخدم هذه البطاقات في أجهزة قراءة البطاقات عند الدخول إلى المصنع والخروج منه.
العمليات المطلوبة:
 INIT() تهيئ النظام، مع افتراض أن المصنع فارغ
 ENTER(p : Person) تسجل دخول عامل إلى المصنع؛ تُقرأ بيانات العامل من بطاقة الهوية
 EXIT(p : Person) تسجل خروج عامل من المصنع
 IS-PRESENT(p : Person) r : bool تتحقق مما إذا كان العامل المحدد موجودًا داخل المصنع أم لا

رسميًا، يكون كما يلي:
 types

 Person = token;
 Workers = set of Person;

 state AWCCS of
   pres: Workers
 end

 operations

 INIT()
 ext wr pres: Workers
 post pres = {};

 ENTER(p : Person)
 ext wr pres : Workers
 pre p not in set pres
 post pres = pres~ union {p};

 EXIT(p : Person)
 ext wr pres : Workers
 pre p in set pres
 post pres = pres~\{p};

 IS-PRESENT(p : Person) r : bool
 ext rd pres : Workers
 post r <=> p in set pres~
بما أن معظم لغات البرمجة تحتوي على مفهوم مشابه للمجموعة (غالبًا في شكل مصفوفة)، فإن الخطوة الأولى من المواصفة هي تمثيل البيانات كسلسلة مرتبة. يجب ألا تسمح هذه السلاسل بالتكرار، لأنه من غير المُرَغّب في ظهور نفس العامل مرتين، لذا يجب إضافة لامتغيرات إلى نوع البيانات الجديد. في هذه الحالة، الترتيب غير مهم، فـ [a,b] تساوي [b,a].

طريقة تطوير فيينا قيمة للأنظمة المبنية على النماذج. لكنها غير مناسبة إذا كان النظام يعتمد على الزمن. في مثل هذه الحالات، يكون حساب الأنظمة التفاعلية أكثر فائدة.

 انظر أيضًا 
 طريقة شكلية
 منطق الرتبة الأولى
 حساب القضايا
 تدوين زد، البديل الرئيسي للغة توصيف طريقة فيينا للتطوير (مقارنة)

 للمزيد من القراءة 



 فيتزجيرالد، ج. س. وLarsen, P.G.، نمذجة الأنظمة: أدوات وتقنيات عملية في هندسة البرمجيات. مطبعة جامعة كامبريدج، 1998  (نُشرت النسخة اليابانية بواسطة إيوانامي شوتن 2003 ).نمذجة الأنظمة: أدوات وتقنيات عملية في هندسة البرمجيات 
 فيتزجيرالد، ج. س.، Larsen, P.G.، Mukherjee, P.، Plat, N. وVerhoef, M.، تصاميم مؤكدة للأنظمة الكائنية التوجه. شبرينغر، 2005. . موقع داعم يحتوي على أمثلة وأدوات مجانية: تصاميم مؤكدة للأنظمة الكائنية التوجه 
 جونز، ك.ب.، تطوير البرمجيات المنهجي باستخدام VDM، برنتس هول، 1990. . متاح أيضاً على الإنترنت مجاناً: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip 
 بيورنر، د. وجونز، ك.ب.، المواصفات الرسمية وتطوير البرمجيات برنتس هول إنترناشيونال، 1982. 
 ج. داوس، دليل مرجعي لـ VDM-SL، بيتمان، 1991. 
 المنظمة الدولية للمعايير، تكنولوجيا المعلومات – لغات البرمجة، بيئاتها وواجهات برمجيات النظام – طريقة فيينا للتطوير – لغة المواصفات – الجزء 1: اللغة الأساسية، المعيار الدولي ISO/IEC 13817-1، ديسمبر 1996.
 جونز، ك.ب.، تطوير البرمجيات: منهج صارم، برنتس هول إنترناشيونال، 1980. 
 جونز، ك.ب. وShaw, R.C. (محرران)، دراسات حالة في تطوير البرمجيات المنهجي، برنتس هول إنترناشيونال، 1990. 
 Bicarregui, J.C.، فيتزجيرالد، ج. س.، ليندسي، ب. أ.، مور، ر. وريتشي، ب..، البرهان في طريقة فيينا للتطوير: دليل الممارس، شبرينغر ضمن سلسلة Formal Approaches to Computing and Information Technology (FACIT)، 1994. .

 المراجع 

 روابط خارجية 
 معلومات عن طريقة فيينا للتطوير وVDM++ (نسخة مؤرشفة في archive.org)
 لغة تعريف فيينا (VDL)
 لغة النمذجة COMPASS  (CML)، وهي مزيج من لغة توصيف طريقة فيينا للتطوير مع العمليات التسلسلية المتواصلة (نموذج حوسبة), مبنية على نظريات توحيد البرمجة، تم تطويرها لنمذجة نظام من النظم (SoS)

تصنيف:طرق شكلية