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

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

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

## التاريخ
تعود أصول لغة توصيف طريقة فيينا للتطوير إلى مختبر آي بي إم في فيينا، حيث أُطلق على أول نسخة من اللغة اسم **لغة تعريف فيينا** (VDL). وقد استُخدمت VDL بشكل أساسي لوصف دلالات التشغيل، بخلاف طريقة فيينا للتطوير – Meta-IV التي قدمت الدلالات التعيينية.

«نحو نهاية عام 1972، عاودت مجموعة فيينا اهتمامها بمشكلة تطوير مترجم من تعريف لغة بطريقة منهجية. وقد أُطلق على النهج العام المتبع اسم "طريقة فيينا للتطوير"... أما اللغة الوصفية التي استُخدمت فعلياً ("ميتا-آي في") فقد استُخدمت لتعريف أجزاء رئيسية من لغة PL/1 (كما وردت في ECMA 74 – وهي وثيقة معايير شكلية مكتوبة كمفسر تجريدي) في BEKIČ 74.»


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

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

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

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

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

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

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

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

```text
types
UserId = nat
```


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

```text
UserId = nat
inv uid == uid <= 9999
```


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

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

على سبيل المثال، عند تمثيل وحدة تحكم إشارات المرور، قد يكون من الملائم تعريف القيم التي تمثل ألوان الإشارة كأنواع اقتباس:

```bnf
<Red>, <Amber>, <FlashingAmber>, <Green>
```


### مُنشئات الأنواع: الاتحاد، والجداء، والأنواع المركبة
الأنواع الأساسية وحدها ذات فائدة محدودة. تُبنى أنواع بيانات جديدة وأكثر تنظيمًا باستخدام مُنشئات الأنواع.

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

```bnf
SignalColour =  <Red> | <Amber> | <FlashingAmber> | <Green>
```


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

يمكن أيضًا تعريف أنواع الجداء الديكارتي في لغة توصيف طريقة فيينا للتطوير. النوع `(A1*…*An)` هو نوع يتكوّن من جميع التُرب المرتبة من القيم، حيث العنصر الأول من النوع `A1` والثاني من النوع `A2` وهكذا. والنوع المركب أو نوع السجل هو جداء ديكارتي مع تسميات للحقول. النوع

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

هو الجداء الديكارتي مع الحقول الموسومة بـ`f1,…,fn`. يمكن تركيب عنصر من النوع `T` من أجزائه المكونة باستخدام المُنشئ المكتوب على الشكل `mk_T`. وعلى العكس، عند إعطاء عنصر من النوع `T`، يمكن استخدام أسماء الحقول لاختيار المكوّن المُسمّى. على سبيل المثال، النوع:

```text
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) إذا رغبت في ذلك. بدمج هذه:

```text
mk_Date(1,4,2001).month = 4
```


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

#### المجموعات
مُنشئ نوع المجموعة (يُكتب `set of T` حيث `T` هو نوع معرف مسبقًا) يُنشئ نوعًا يتكوّن من جميع المجموعات المنتهية من القيم المأخوذة من النوع `T`. على سبيل المثال، يُعرّف تعريف النوع التالي:

```rsl
UGroup = set of UserId
```

نوع `UGroup` بوصفه مجموعة منتهية من القيم من نوع `UserId`. وتوجد العديد من المعاملات المعرفة على المجموعات لبناء اتحادها، وتقاطعها، وتحديد العلاقات بين المجموعات الجزئية الصارمة وغير الصارمة، وغيرها.

#### التسلسلات
مُنشئ نوع التسلسل المنتهي (يُكتب `seq of T` حيث `T` هو نوع معرف مسبقًا) يُنشئ نوعًا يتكوّن من جميع القوائم المنتهية من القيم المأخوذة من النوع `T`. على سبيل المثال، يُعرّف تعريف النوع التالي:

```rsl
String = seq of char
```

نوع `String` بوصفه جميع السلاسل النصية المنتهية من الحروف. توجد عدة معاملات معرفة على التسلسلات لبناء السلاسل، واختيار العناصر، واستخراج تسلسلات فرعية، وغيرها. العديد من هذه المعاملات جزئية، بمعنى أنها غير معرفة لبعض التطبيقات. على سبيل المثال، اختيار العنصر الخامس من تسلسل يحتوي على ثلاثة عناصر فقط غير معرّف.

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

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

```rsl
Birthdays = map String to Date
```

يُعرّف نوعًا اسمه `Birthdays` يربط سلاسل الأحرف إلى `Date`. ويوجد عدد من المعاملات المعرفة على الخرائط مثل الفهرسة داخل الخريطة، دمج الخرائط، والكتابة فوقها واستخراج خرائط فرعية.

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

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

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

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

على سبيل المثال، يمكن تعريف دالة `SQRT` لحساب الجذر التربيعي لعدد طبيعي كما يلي:

```rsl
SQRT(x:nat)r:real
post r*r = x
```

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

يمكن الحصول على مواصفة أكثر تقييدًا للدالة عن طريق تقوية شرط ما بعد التنفيذ. على سبيل المثال، التعريف التالي يُقيّد الدالة بإرجاع الجذر الموجب فقط:

```rsl
SQRT(x:nat)r:real
post r*r = x and r>=0
```

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

```rsl
SQRTP(x:real)r:real
pre x >=0
post r*r = x and r>=0
```

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

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

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

يتكوَّن هذا التعريف التكراري من توقيع للدالة يحدد نوعي المُدخل والنتيجة، وجسم دالة يوضح آلية الحساب. أما تعريف الدالة الضمني نفسه فيمكن أن يأخذ الشكل التالي:

```rsl
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
```

يمكن اعتبار التعريف الصريح تنفيذًا مباشرًا للدالة المحددة ضمنيًا. وتُحدد صحة التعريف الصريح بالنسبة إلى المواصفة الضمنية كما يلي:

بالنظر إلى المواصفة الضمنية:

```rsl
f(p:T_p)r:T_r
pre pre-f(p)
post post-f(p, r)
```

ودالة صريحة:

```rsl
f:T_p -> T_r
```

فإننا نقول إنها تحقق المواصفة إذا وفقط إذا:

```rsl
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`، فيمكن تعريف هذه الحالة في لغة توصيف طريقة فيينا للتطوير كما يلي:

```rsl
state Register of
  someStateRegister : nat
end
```

أما في VDM++، فسيتم تعريفها كالتالي:

```rsl
instance variables
  someStateRegister : nat
```

ويمكن تحديد عملية لتحميل قيمة إلى هذا المتغير كما يلي:

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

تُحدد جملة "الخارجيات" (`ext`) الأجزاء من الحالة التي يمكن للعملية الوصول إليها؛ حيث يشير `rd` إلى الوصول للقراءة فقط، و`wr` إلى الوصول للقراءة والكتابة.

وفي بعض الأحيان، من المهم الرجوع إلى قيمة الحالة قبل تعديلها؛ فمثلًا، يمكن تحديد عملية لإضافة قيمة إلى المتغير كما يلي:

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

حيث تشير العلامة `~` على متغير الحالة في شرط ما بعد التنفيذ إلى قيمة المتغير قبل تنفيذ العملية.

## أمثلة

### دالة ''ماكس''
هذه مثال لتعريف دالة ضمنية. تقوم هذه الدالة بإرجاع العنصر الأكبر من مجموعة من الأعداد الطبيعية:

```rsl
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` إذا كانت المجموعة فارغة.

### الضرب للأعداد الطبيعية

```rsl
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`:

```rsl
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)
```

فإن التزام الإثبات يصبح:

```rsl
forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j
```

ويمكن إثبات صحة ذلك عبر:
# إثبات أن الاستدعاء التكراري ينتهي (وهذا بدوره يتطلب إثبات أن الأعداد تصبح أصغر في كل خطوة)
# استقراء رياضي

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

```rsl
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`). وتمثيلات أرقام العملاء تُعد غير مهمة ولذلك يُعبَّر عنها كنوع رمز. أما الأرصدة والسُحوبات المكشوفة فتُنمذج بأنواع عددية.

```rsl
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* بتخصيص رقم عميل جديد:

```rsl
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* بتخصيص رقم حساب جديد وتعيين الرصيد إلى صفر:

```rsl
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* جميع أرصدة حسابات عميل ما، كخريطة من رقم الحساب إلى الرصيد:

```rsl
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 في الدنمارك وشركة سي إس كيه القابضة في اليابان.
* تريد ون: تم تطوير بعض المكونات الرئيسية لنظام تريد ون الخلفي من قبل أنظمة سي إس كي لبورصة طوكيو باستخدام طريقة فيينا للتطوير. وتوجد قياسات مقارنة لإنتاجية المطورين وكثافة العيوب للمكونات المطورة بـ طريقة فيينا للتطوير مقابل الكود المطور بالطريقة التقليدية.
* أبلغت شبكات فيليكا عن تطوير نظام تشغيل لدارة متكاملة لتطبيقات الهاتف المحمول.

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

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

:\begin{array}
\textbf{Specification}
& &
\textbf{Implementation}
\\
\hline
\text{نوع بيانات مجرد} &
\xrightarrow\text{تجسيد البيانات} &
\text{بنية بيانات}
\\
\text{عمليات} &
\xrightarrow[\text{تفكيك العمليات}]{} &

\text{خوارزميات}
\end{array}

### تجسيد البيانات
تجسيد البيانات (التحسين خطوة بخطوة) ينطوي على إيجاد تمثيل أكثر تحديدًا لأنواع البيانات المجردة المستخدمة في المواصفة. قد تكون هناك عدة خطوات قبل الوصول إلى التنفيذ. كل خطوة تجسيد لتمثيل بيانات مجرد `ABS_REP` تتطلب اقتراح تمثيل جديد `NEW_REP`. لإثبات دقة التمثيل الجديد، يتم تعريف دالة *استرجاع* تربط `NEW_REP` بـ `ABS_REP`، أي `retr : NEW_REP -> ABS_REP`. تعتمد صحة تجسيد البيانات على إثبات *الكفاية*، أي:

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

وبما أن تمثيل البيانات قد تغير، من الضروري تحديث العمليات والدوال لتعمل على `NEW_REP`. يجب إثبات أن العمليات والدوال الجديدة تحافظ على أي لامتغير (رياضيات) لنوع البيانات على التمثيل الجديد. ولإثبات أن العمليات والدوال الجديدة تحاكي تلك الموجودة في المواصفة الأصلية، يجب الوفاء بواجبين برهانيين:
* قاعدة النطاق (Domain rule):

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

* قاعدة النمذجة (Modelling rule):

```rsl
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` تتحقق مما إذا كان العامل المحدد موجودًا داخل المصنع أم لا

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

```rsl
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. . موقع داعم يحتوي على أمثلة وأدوات مجانية: http://www.vdmbook.com
* جونز، ك.ب.، *تطوير البرمجيات المنهجي باستخدام 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)

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