أسلوب فيينا للتطوير
تُعدّ طريقة فيينا للتطوير ( VDM ) من أقدم الطرق الرسمية لتطوير الأنظمة الحاسوبية. نشأت هذه الطريقة في مختبر IBM في فيينا [ 1 ] خلال سبعينيات القرن الماضي، وتطورت لتشمل مجموعة من التقنيات والأدوات القائمة على لغة مواصفات رسمية تُعرف باسم لغة مواصفات VDM (VDM-SL). ولها نسخة موسعة، VDM++ [ 2 ] ، تدعم نمذجة الأنظمة الموجهة للكائنات والأنظمة المتزامنة. وتشمل أدوات دعم VDM أدوات تجارية وأكاديمية لتحليل النماذج، بما في ذلك دعم اختبار خصائص النماذج وإثباتها، وتوليد شفرة برمجية من نماذج VDM المُدققة. ولطريقة فيينا للتطوير وأدواتها تاريخ طويل من الاستخدام الصناعي، وقد أدى تزايد الأبحاث في هذا المجال إلى إسهامات بارزة في هندسة الأنظمة الحساسة، والمترجمات ، والأنظمة المتزامنة، وفي منطق علوم الحاسوب .
فلسفة
يمكن نمذجة أنظمة الحوسبة باستخدام لغة VDM-SL بمستوى تجريد أعلى مما هو ممكن باستخدام لغات البرمجة، مما يسمح بتحليل التصاميم وتحديد السمات الرئيسية، بما في ذلك العيوب، في مرحلة مبكرة من تطوير النظام. ويمكن تحويل النماذج التي تم التحقق من صحتها إلى تصاميم نظام مفصلة من خلال عملية تحسين. تتميز اللغة بدلالات رسمية، مما يتيح إثبات خصائص النماذج بمستوى عالٍ من الموثوقية. كما أنها تحتوي على مجموعة فرعية قابلة للتنفيذ، بحيث يمكن تحليل النماذج عن طريق الاختبار، ويمكن تنفيذها من خلال واجهات المستخدم الرسومية، مما يتيح تقييم النماذج من قبل خبراء ليسوا بالضرورة على دراية بلغة النمذجة نفسها.
تاريخ
تعود أصول لغة VDM-SL إلى مختبر IBM في فيينا ، حيث سُميت النسخة الأولى منها بلغة تعريف فيينا ( VDL). [ 3 ] استُخدمت لغة VDL بشكل أساسي لتقديم أوصاف دلالية تشغيلية ، على عكس لغة VDM – Meta-IV التي قدمت دلالات وصفية . [ 4 ]
«مع اقتراب نهاية عام 1972، وجّهت مجموعة فيينا اهتمامها مجدداً إلى مشكلة التطوير المنهجي للمترجم انطلاقاً من تعريف اللغة. وقد أُطلق على النهج العام المُعتمد اسم "طريقة فيينا للتطوير"... تُستخدم اللغة الوصفية المُعتمدة فعلياً ("Meta-IV") لتعريف أجزاء رئيسية من لغة PL/1 (كما ورد في ECMA 74 - وهو، من المثير للاهتمام، "وثيقة معايير رسمية مكتوبة كمترجم تجريدي") في BEKIČ 74.» [ 5 ]
لا توجد علاقة بين Meta-IV ، [ 6 ] ولغة META II الخاصة بـ Schorre ، أو خليفتها Tree Meta ؛ كانت هذه أنظمة مترجم-مترجم بدلاً من كونها مناسبة لوصف المشكلات الرسمية.
لذا، استُخدمت لغة Meta-IV لتحديد أجزاء رئيسية من لغة البرمجة PL/I . ومن لغات البرمجة الأخرى التي وُصفت، كليًا أو جزئيًا، باستخدام Meta-IV وVDM-SL، لغة البرمجة BASIC ، ولغة FORTRAN ، ولغة APL ، ولغة ALGOL 60، ولغة Ada ، ولغة Pascal . وقد تطورت Meta-IV إلى عدة صيغ، تُعرف عمومًا بالمدارس الدنماركية والإنجليزية والأيرلندية.
انبثقت "المدرسة الإنجليزية" من أعمال كليف جونز حول جوانب VDM غير المرتبطة تحديدًا بتعريف اللغة وتصميم المترجمات (جونز 1980، 1990). وتركز هذه المدرسة على نمذجة الحالة المستمرة [ 7 ] باستخدام أنواع البيانات المُنشأة من مجموعة غنية من الأنواع الأساسية. وعادةً ما تُوصف الوظائف من خلال عمليات قد يكون لها آثار جانبية على الحالة، والتي تُحدد في الغالب ضمنيًا باستخدام شرط مسبق وشرط لاحق. أما "المدرسة الدنماركية" ( بيورنر وآخرون، 1982) فقد مالت إلى التركيز على منهج بنائي مع استخدام مواصفات تشغيلية صريحة على نطاق أوسع. وقد أدى العمل في المدرسة الدنماركية إلى أول مترجم أوروبي مُعتمد للغة آدا .
تم إصدار معيار ISO للغة في عام 1996 (ISO، 1996).
ميزات VDM
يُشرح بناء جملة ودلالات لغتي VDM-SL وVDM++ بالتفصيل في أدلة لغة VDMTools والنصوص المتاحة. يتضمن معيار ISO تعريفًا رسميًا لدلالات اللغة. في بقية هذه المقالة، يُستخدم بناء جملة التبادل (ASCII) المُعرّف من قِبل ISO. تُفضّل بعض النصوص استخدام بناء جملة رياضي أكثر إيجازًا .
نموذج VDM-SL هو وصف للنظام يُقدم من حيث الوظائف التي تُنفذ على البيانات. ويتكون من سلسلة من تعريفات أنواع البيانات والوظائف أو العمليات التي تُنفذ عليها.
الأنواع الأساسية: الأنواع الرقمية، والحرفية، والرموز، وعلامات الاقتباس
يتضمن VDM-SL أنواعًا أساسية لنمذجة الأرقام والحروف على النحو التالي:
bool | القيم المنطقية | خطأ، صحيح |
nat | الأعداد الطبيعية (بما في ذلك الصفر) | ٠، ١، ٢، ٣، ٤، ٥ ... |
nat1 | الأعداد الطبيعية (باستثناء الصفر) | 1، 2، 3، 4، 5، ... |
int | الأعداد الصحيحة | ..., −3, −2, −1, 0, 1, 2, 3, ... |
rat | الأعداد النسبية | a/b ، حيث a و b عددان صحيحان، و b لا يساوي صفرًا |
real | أرقام حقيقية | ... |
char | الشخصيات | أ، ب، ج، ... |
token | رموز غير مهيكلة | ... |
<A> | نوع الاقتباس الذي يحتوي على القيمة<A> | ... |
تُعرَّف أنواع البيانات لتمثيل البيانات الرئيسية للنظام المُنمذج. يُقدِّم كل تعريف نوع اسم نوع جديد، ويُعطي تمثيلاً له بدلالة الأنواع الأساسية أو بدلالة الأنواع المُعرَّفة سابقاً. على سبيل المثال، قد يُعرَّف نوع يُنمذج مُعرِّفات المستخدمين لنظام إدارة تسجيل الدخول كما يلي:
أنواع معرف المستخدم = nat لمعالجة القيم التي تنتمي إلى أنواع البيانات، تُعرَّف عوامل تشغيل على هذه القيم. وهكذا، تُوفَّر عمليات جمع وطرح الأعداد الطبيعية، بالإضافة إلى عوامل التشغيل المنطقية مثل المساواة وعدم المساواة. لا تُحدِّد اللغة حدًا أقصى أو أدنى لعدد قابل للتمثيل، أو دقة للأعداد الحقيقية. تُعرَّف هذه القيود عند الحاجة إليها في كل نموذج باستخدام ثوابت نوع البيانات - وهي تعابير منطقية تُشير إلى الشروط التي يجب أن تُراعيها جميع عناصر النوع المُعرَّف. على سبيل المثال، يُعبَّر عن شرط ألا تتجاوز مُعرِّفات المستخدم 9999 كما يلي (حيث <=يُمثِّل عامل التشغيل المنطقي "أصغر من أو يساوي" للأعداد الطبيعية):
معرف المستخدم = nat inv uid == uid <= 9999 بما أن الثوابت يمكن أن تكون تعبيرات منطقية معقدة بشكل تعسفي، وعضوية نوع محدد تقتصر فقط على تلك القيم التي تحقق الثابت، فإن صحة النوع في VDM-SL لا يمكن تحديدها تلقائيًا في جميع الحالات.
تشمل الأنواع الأساسية الأخرى char للأحرف. في بعض الحالات، لا يكون تمثيل نوع ما ذا صلة بهدف النموذج، بل قد يزيد من تعقيده. في مثل هذه الحالات، يمكن تمثيل عناصر النوع كرموز غير مُهيكلة. لا يمكن مقارنة قيم أنواع الرموز إلا من حيث التساوي، ولا تُعرَّف عليها أي عوامل أخرى. عند الحاجة إلى قيم مُسماة مُحددة، تُعرَّف هذه القيم كأنواع اقتباس. يتكون كل نوع اقتباس من قيمة مُسماة واحدة تحمل نفس اسم النوع نفسه. لا يمكن مقارنة قيم أنواع الاقتباس (المعروفة باسم القيم الحرفية للاقتباس) إلا من حيث التساوي.
على سبيل المثال، عند تصميم نموذج لجهاز تحكم إشارات المرور، قد يكون من الملائم تحديد قيم لتمثيل ألوان إشارة المرور كأنواع اقتباس:
< أحمر > ، < كهرماني > ، < كهرماني وامض > ، < أخضر >مُنشئات الأنواع: أنواع الاتحاد، والضرب، والأنواع المركبة
لا تُعدّ الأنواع الأساسية وحدها ذات قيمة كبيرة. أما أنواع البيانات الجديدة والأكثر تنظيماً فتُبنى باستخدام مُنشئات الأنواع.
T1 | T2 | ... | Tn | اتحاد الأنواعT1,...,Tn |
T1*T2*...*Tn | حاصل الضرب الديكارتي لأنواعT1,...,Tn |
T :: f1:T1 ... fn:Tn | نوع مركب (سجل) |
يُشكّل مُنشئ النوع الأساسي اتحاد نوعين مُعرّفين مُسبقًا. (A|B)يحتوي النوع على جميع عناصر النوع A وجميع عناصر النوع B. في مثال وحدة تحكم إشارات المرور، يُمكن تعريف النوع الذي يُمثّل لون إشارة المرور على النحو التالي:
لون الإشارة = < أحمر > | < كهرماني > | < كهرماني وامض > | < أخضر >يتم تعريف الأنواع المعدودة في VDM-SL كما هو موضح أعلاه كاتحادات على أنواع الاقتباس.
يمكن أيضًا تعريف أنواع الضرب الديكارتي في VDM-SL. النوع (A1*…*An)هو النوع المُكوَّن من جميع صفوف القيم، حيث يكون العنصر الأول من النوع الأول A1والثاني من النوع الثاني، A2وهكذا. النوع المركب أو نوع السجل هو ضرب ديكارتي مع تسميات للحقول.
T :: f1:A1 f2:A2 ... fn:An هو حاصل الضرب الديكارتي مع الحقول المُسماة f1,…,fn. يمكن تكوين عنصر من النوع Tمن أجزائه المكونة بواسطة مُنشئ، يُكتب mk_T. على العكس من ذلك، عند إعطاء عنصر من النوع T، يمكن استخدام أسماء الحقول لتحديد المكون المُسمى. على سبيل المثال، النوع
التاريخ :: اليوم: التاريخ الطبيعي 1 الشهر: نات1 السنة: طبيعي inv mk_Date(d,m,y) == d<=31 and m<=12 يُمثل هذا النموذج نوع تاريخ بسيط. القيمة mk_Date(1,4,2001)تُشير إلى 1 أبريل 2001. عند إدخال تاريخ d، يكون التعبير d.monthعددًا طبيعيًا يُمثل الشهر. يُمكن إضافة قيود على عدد أيام الشهر والسنوات الكبيسة إلى الثابت إذا لزم الأمر. بدمج هذه العناصر:
mk_Date(1,4,2001).month = 4 المجموعات
تُمثل أنواع المجموعات مجموعات من القيم. المجموعات هي مجموعات محدودة غير مرتبة، حيث يُمنع تكرار القيم. أما المتتاليات فهي مجموعات محدودة مرتبة (قوائم) قد يحدث فيها تكرار، وتمثل عمليات الربط علاقات محدودة بين مجموعتين من القيم.
مجموعات
يقوم مُنشئ نوع المجموعة (المكتوب set of Tحيث Tيكون نوعًا مُعرَّفًا مسبقًا) بإنشاء النوع المُكوَّن من جميع المجموعات المحدودة من القيم المُستمدة من النوع T. على سبيل المثال، تعريف النوع
مجموعة UGroup = مجموعة من معرفات المستخدميُعرّف نوعاً UGroupيتألف من جميع المجموعات المنتهية من UserIdالقيم. تُعرّف عوامل تشغيلية متنوعة على المجموعات لإنشاء اتحادها، وتقاطعاتها، وتحديد علاقات المجموعات الجزئية الصحيحة وغير الصارمة، وما إلى ذلك.
{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تتألف من جميع السلاسل النصية المحدودة. تُعرّف عوامل تشغيلية متنوعة على هذه السلاسل لإنشاء عمليات الربط، واختيار العناصر، والسلاسل الفرعية، وما إلى ذلك. العديد من هذه العوامل جزئية، بمعنى أنها غير مُعرّفة لبعض التطبيقات. على سبيل المثال، اختيار العنصر الخامس من سلسلة تحتوي على ثلاثة عناصر فقط غير مُعرّف.
يُعد ترتيب العناصر وتكرارها في التسلسل أمرًا مهمًا، لذا [a, b]فإن لا يساوي [b, a]، ولا [a]يساوي [a, a].
[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) | العنصر iرقم 1 منs |
inds s | مجموعة المؤشرات الخاصة بالتسلسلs |
s1^s2 | التسلسل المتكون من خلال دمج التسلسلات s1وs2 |
خرائط
التطبيق المحدود هو علاقة تناظر بين مجموعتين، المجال والمدى، حيث يشير المجال إلى عناصر المدى. ولذلك فهو مشابه للدالة المحدودة. يقوم مُنشئ نوع التطبيق في VDM-SL (المكتوب map T1 to T2حيث T1و T2نوعان مُعرّفان مسبقًا) بإنشاء النوع المُكوّن من جميع التطبيقات المحدودة من مجموعات T1القيم إلى مجموعات T2القيم. على سبيل المثال، تعريف النوع
أعياد الميلاد = تحويل السلسلة النصية إلى تاريخيُعرّف نوعًا 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-SL و VDM++ في طريقة التعامل مع البنية. ففي VDM-SL، يوجد امتداد معياري تقليدي، بينما في VDM++، توجد آلية بنية تقليدية موجهة للكائنات مع الفئات والوراثة.
الهيكلة في VDM-SL
يحتوي معيار ISO الخاص بـ VDM-SL على ملحق إرشادي يتضمن مبادئ هيكلية مختلفة. تتبع هذه المبادئ جميعها مبادئ إخفاء المعلومات التقليدية باستخدام الوحدات، ويمكن شرحها على النحو التالي:
- تسمية الوحدات : تبدأ كل وحدة نحويًا بالكلمة المفتاحية
moduleمتبوعة باسم الوحدة. وفي نهاية الوحدة،endتُكتب الكلمة المفتاحية متبوعة مرة أخرى باسم الوحدة. - الاستيراد : من الممكن استيراد التعريفات المُصدَّرة من وحدات أخرى. يتم ذلك في قسم الاستيرادات الذي يبدأ بالكلمة المفتاحية،
importsمتبوعًا بسلسلة من عمليات الاستيراد من وحدات مختلفة. يبدأ كل استيراد من هذه الاستيرادات بالكلمة المفتاحية،fromمتبوعة باسم الوحدة وتوقيعها. يمكن أن يكون توقيع الوحدة ببساطة الكلمة المفتاحيةallالتي تشير إلى استيراد جميع التعريفات المُصدَّرة من تلك الوحدة، أو يمكن أن يكون سلسلة من توقيعات الاستيراد. توقيعات الاستيراد خاصة بالأنواع والقيم والدوال والعمليات، ويبدأ كل منها بالكلمة المفتاحية المناسبة. بالإضافة إلى ذلك، تُسمّي توقيعات الاستيراد هذه البنى التي يُراد الوصول إليها. كما يمكن إضافة معلومات اختيارية عن النوع، وأخيرًا، من الممكن إعادة تسمية كل بنية عند الاستيراد. بالنسبة للأنواع، يجب أيضًا استخدام الكلمة المفتاحيةstructللوصول إلى البنية الداخلية لنوع معين. - التصدير : تُصدَّر التعريفات من وحدة نمطية، التي يرغب المستخدم في أن تتمكن الوحدات النمطية الأخرى من الوصول إليها، باستخدام الكلمة المفتاحية `exports`
exportsمتبوعةً بتوقيع الوحدة النمطية `exports`. يمكن أن يتكون توقيع الوحدة النمطية `exports` إما من الكلمة المفتاحية `exports` فقطall، أو كسلسلة من توقيعات التصدير. تُخصَّص توقيعات التصدير هذه لأنواع وقيم ووظائف وعمليات محددة، ويبدأ كل منها بالكلمة المفتاحية المناسبة. في حال الرغبة في تصدير البنية الداخلية لنوع ما،structيجب استخدام الكلمة المفتاحية `exports`. - ميزات إضافية : في الإصدارات السابقة من VDM-SL، كانت الأدوات تدعم الوحدات النمطية المُعَلمة وإنشاء نسخ منها. مع ذلك، أُزيلت هذه الميزات من VDMTools حوالي عام 2000 نظرًا لقلة استخدامها في التطبيقات الصناعية، ولوجود عدد كبير من التحديات التي واجهتها الأدوات فيما يتعلق بهذه الميزات.
الهيكلة في VDM++
في VDM++، يتم تنظيم البنية باستخدام الفئات والوراثة المتعددة . المفاهيم الأساسية هي:
- الفئة : تبدأ كل فئة نحويًا بالكلمة المفتاحية
classمتبوعة باسم الفئة. وفي نهاية الفئة،endتُكتب الكلمة المفتاحية متبوعة مرة أخرى باسم الفئة. - الوراثة : في حالة وراثة فئة ما لبنى من فئات أخرى، يمكن أن يتبع اسم الفئة في عنوان الفئة الكلمات الرئيسية
is subclass ofمتبوعة بقائمة مفصولة بفواصل لأسماء الفئات العليا. - مُعدِّلات الوصول : يتم إخفاء المعلومات في VDM++ بنفس طريقة معظم لغات البرمجة الكائنية باستخدام مُعدِّلات الوصول. في VDM++، تكون التعريفات خاصة افتراضيًا، ولكن يُمكن استخدام إحدى كلمات مُعدِّلات الوصول أمام جميع التعريفات: `private`
privateو`publicprivate` و`protectedprivate`.
وظائف النمذجة
النمذجة الوظيفية
في لغة VDM-SL، تُعرَّف الدوال على أنواع البيانات المُعرَّفة في النموذج. يتطلب دعم التجريد إمكانية تحديد النتيجة التي يجب أن تحسبها الدالة دون الحاجة إلى تحديد كيفية حسابها. الآلية الرئيسية لتحقيق ذلك هي تعريف الدالة الضمني ، حيث يُستخدم شرط منطقي على متغيرات الإدخال والنتيجة، يُسمى الشرط اللاحق ، بدلاً من صيغة رياضية لحساب النتيجة. على سبيل المثال، يمكن تعريف دالة SQRTلحساب الجذر التربيعي لعدد طبيعي كما يلي:
الجذر التربيعي (x:الطبيعي)r: عدد حقيقي r*r = x هنا، لا يُحدد الشرط اللاحق طريقةً لحساب النتيجة، rبل يُحدد الخصائص التي يُمكن افتراض تحققها فيها. لاحظ أن هذا يُعرّف دالةً تُعيد جذرًا تربيعيًا صحيحًا؛ ولا يُشترط أن يكون الجذر موجبًا أو سالبًا. على سبيل المثال، يُمكن تحقيق المواصفات المذكورة أعلاه بدالة تُعيد الجذر السالب للعدد 4، والجذر الموجب لجميع المدخلات الصحيحة الأخرى. تجدر الإشارة إلى أن الدوال في لغة VDM-SL يجب أن تكون حتمية، بحيث يجب على الدالة التي تُحقق مواصفات المثال أعلاه أن تُعيد دائمًا نفس النتيجة لنفس المدخل.
يُمكن الوصول إلى مواصفات دالة أكثر تقييدًا من خلال تعزيز الشرط اللاحق. على سبيل المثال، يُقيد التعريف التالي الدالة بحيث تُعيد الجذر الموجب.
الجذر التربيعي (x:الطبيعي)r: عدد حقيقي r*r = x و r >= 0قد تخضع جميع مواصفات الدوال لشروط مسبقة، وهي عبارة عن دوال منطقية تُطبق على متغيرات الإدخال فقط، وتصف القيود التي يُفترض تحققها عند تنفيذ الدالة. على سبيل المثال، يمكن تحديد دالة حساب الجذر التربيعي التي تعمل فقط على الأعداد الحقيقية الموجبة كما يلي:
SQRTP (x: عدد حقيقي )r: عدد حقيقي pre x >= 0 post 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: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نقول إنها تفي بالمواصفات إذا وفقط إذا :
لكل p في المجموعة T_p و pre -f(p) => f(p): T_r و post -f(p, f(p)) لذا، fيجب تفسير عبارة "هو تطبيق صحيح" على أنها " fيلبي المواصفات".
النمذجة القائمة على الحالة
في لغة VDM-SL، لا تُحدث الدوال آثارًا جانبية مثل تغيير حالة متغير عام ثابت . هذه ميزة مفيدة في العديد من لغات البرمجة، لذا يوجد مفهوم مشابه؛ فبدلاً من الدوال، تُستخدم العمليات لتغيير متغيرات الحالة (المعروفة أيضًا بالمتغيرات العامة ).
على سبيل المثال، إذا كان لدينا حالة تتكون من متغير واحد ، فيمكننا تعريف ذلك في VDM-SL على النحو التالي:someStateRegister : nat
سجل الولاية لـ someStateRegister : nat endفي VDM++، سيتم تعريف ذلك على النحو التالي:
متغيرات النسخة someStateRegister : nat يمكن تحديد عملية تحميل قيمة في هذا المتغير على النحو التالي:
تحميل (i:nat) تحويلة wr someStateRegister:nat post someStateRegister = i تحدد عبارة externals ( ext) أجزاء الحالة التي يمكن الوصول إليها بواسطة العملية؛ rdمما يشير إلى الوصول للقراءة فقط wrوكونها وصولًا للقراءة/الكتابة.
في بعض الأحيان يكون من المهم الإشارة إلى قيمة الحالة قبل تعديلها؛ على سبيل المثال، يمكن تحديد عملية إضافة قيمة إلى المتغير على النحو التالي:
ADD (i:nat) ext wr someStateRegister : nat post someStateRegister = someStateRegister~ + i حيث ~يشير الرمز الموجود على متغير الحالة في الشرط اللاحق إلى قيمة متغير الحالة قبل تنفيذ العملية.
أمثلة
دالة الحد الأقصى
هذا مثال على تعريف دالة ضمنية. تُعيد الدالة أكبر عنصر من مجموعة الأعداد الصحيحة الموجبة:
أقصى (s: مجموعة من nat)r: nat قبل البطاقة s > 0 بعد r في المجموعة s و لكل r' في المجموعة 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) == إذا كان i= 0 فإن 0، وإذا كان i سالبًا زوجيًا فإن 2 *multp(i/ 2 ,j)، وإلا فإن j+multp(i- 1 ,j) ثم يصبح الالتزام بالإثبات كما يلي:
لكل i و j : nat و multp(i,j) :nat و multp(i, j) = i*j ويمكن إثبات صحة ذلك من خلال:
- إثبات أن التكرار ينتهي (وهذا بدوره يتطلب إثبات أن الأرقام تصبح أصغر في كل خطوة)
- الاستقراء الرياضي
نوع بيانات مجردة للصف
هذا مثال كلاسيكي يوضح استخدام تحديد العمليات الضمني في نموذج قائم على الحالة لبنية بيانات معروفة. يتم نمذجة الطابور كسلسلة مكونة من عناصر من نوع معين Qelt. التمثيل Qeltغير مهم، لذا يُعرَّف كنوع رمزي.
أنواع Qelt = رمز مميز ؛ Queue = تسلسل Qelt ؛حالة قائمة الانتظار q : نهاية قائمة الانتظارالعمليات 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 ) مثال على النظام المصرفي
كمثال بسيط جدًا على نموذج VDM-SL، لنفترض نظامًا لحفظ تفاصيل الحسابات المصرفية للعملاء. يُمثل العملاء بأرقامهم ( CustNum )، وتُمثل الحسابات بأرقامها ( AccNum ). تُعتبر تمثيلات أرقام العملاء غير مهمة، لذا تُمثل بنوع رمزي. أما الأرصدة والسحب على المكشوف فتُمثل بأنواع رقمية.
رقم الحساب = رمز مميز؛ رقم العميل = رمز مميز؛ الرصيد = عدد صحيح ؛ السحب على المكشوف = طبيعي؛بيانات الحساب :: المالك : رقم العميل الرصيد : الرصيدحالة البنك من accountMap : ربط رقم الحساب ببيانات الحساب overdraftMap : ربط رقم العميل ببيانات السحب على المكشوف inc mk_Bank(accountMap , overdraftMap) == لكل a في مجموعة rng accountMap و a.owner في مجموعة dom overdraftMap و a.balance >= -overdraftMap(a.owner) مع العمليات: تقوم NEWC بتخصيص رقم عميل جديد:
عمليات NEWC (od : Overdraft )r : CustNum ext wr overdraftMap : ربط CustNum بـ 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 : ربط رقم الحساب بالرصيد ext rd accountMap : ربط رقم الحساب ببيانات الحساب post r = {an | -> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu} دعم الأدوات
يدعم عدد من الأدوات المختلفة إدارة الأجهزة الافتراضية (VDM):
- كانت VDMTools الأداة التجارية الرائدة لـ VDM وVDM++، مملوكة ومسوقة ومُدارة ومطورة من قبل شركة CSK Systems ، استنادًا إلى إصدارات سابقة طورتها شركة IFAD الدنماركية. تتوفر الأدلة ودليل عملي (مؤرشف بتاريخ 19 نوفمبر 2008 على موقع Wayback Machine) . جميع التراخيص متاحة مجانًا للنسخة الكاملة من الأداة. تتضمن النسخة الكاملة توليدًا تلقائيًا للتعليمات البرمجية للغتين Java وC++، ومكتبة الارتباط الديناميكي، ودعم CORBA.
- أوفرتشر هي مبادرة مفتوحة المصدر قائمة على المجتمع، تهدف إلى توفير دعم مجاني للأدوات لجميع لهجات VDM (VDM-SL وVDM++ وVDM-RT)، والتي كانت في الأصل مبنية على منصة Eclipse، ثم أصبحت لاحقًا مبنية على منصة Visual Studio Code. ويهدف المشروع إلى تطوير إطار عمل لأدوات قابلة للتشغيل البيني، تُفيد في التطبيقات الصناعية والبحثية والتعليمية.
- vdm-mode عبارة عن مجموعة من حزم Emacs لكتابة مواصفات VDM باستخدام VDM-SL وVDM++ وVDM-RT. وهي تدعم تمييز وتحرير بناء الجملة، والتحقق من بناء الجملة أثناء التشغيل، وإكمال القوالب، ودعم المفسر.
- أُرشف SpecBox في 7 يوليو 2011 على موقع Wayback Machine : من تطوير أديلارد، يوفر فحصًا نحويًا، وبعض الفحوصات الدلالية البسيطة، وإنشاء ملف LaTeX يُمكّن من طباعة المواصفات باستخدام الترميز الرياضي. هذه الأداة متاحة مجانًا، ولكنها لم تعد تُحدَّث.
- تتوفر وحدات ماكرو LaTeX وLaTeX2e لدعم عرض نماذج VDM باستخدام الصيغة الرياضية للغة ISO القياسية. وقد طُوّرت هذه الوحدات وتُدار من قِبل المختبر الفيزيائي الوطني في المملكة المتحدة. تتوفر الوثائق ووحدات الماكرو عبر الإنترنت.
الخبرة الصناعية
تم تطبيق تقنية VDM على نطاق واسع في مجالات تطبيقية متنوعة. ومن أبرز هذه التطبيقات ما يلي:
- مترجمات لغة Ada و CHILL : طُوِّر أول مترجم لغة Ada أوروبي معتمد من قِبَل مركز Dansk Datamatik باستخدام VDM. [ 8 ] وبالمثل، وُصِفت دلالات CHILL و Modula-2 في معاييرهما باستخدام VDM.
- ConForm: تجربة في شركة British Aerospace تقارن بين التطوير التقليدي لبوابة موثوقة والتطوير باستخدام VDM.
- Dust-Expert: مشروع نفذته شركة Adelard في المملكة المتحدة لتطبيق متعلق بالسلامة لتحديد مدى ملاءمة السلامة في تصميم المصانع الصناعية.
- تطوير VDMTools: تم تطوير معظم مكونات مجموعة أدوات VDMTools باستخدام VDM. وقد تم هذا التطوير في IFAD في الدنمارك و CSK في اليابان . [ 9 ]
- TradeOne: تم تطوير بعض المكونات الرئيسية لنظام TradeOne، وهو نظام إدارة خلفية للبورصة اليابانية، بواسطة شركة CSK Systems باستخدام تقنية VDM. وتتوفر قياسات مقارنة لإنتاجية المطورين وكثافة العيوب في المكونات المطورة باستخدام VDM مقارنةً بالكود المطوّر بالطريقة التقليدية.
- أعلنت شركة FeliCa Networks عن تطوير نظام تشغيل لدائرة متكاملة لتطبيقات الهواتف الخلوية .
التحسين
يبدأ استخدام VDM بنموذج مجرد للغاية ثم يطوره إلى تطبيق عملي. تتضمن كل خطوة إعادة تجسيد البيانات ، ثم تجزئة العمليات .
يعمل تجسيد البيانات على تطوير أنواع البيانات المجردة إلى هياكل بيانات أكثر واقعية ، بينما يعمل تفكيك العمليات على تطوير المواصفات الضمنية (المجردة) للعمليات والوظائف إلى خوارزميات يمكن تنفيذها مباشرة بلغة حاسوب مختارة.
![{\displaystyle {\begin{array}{|rcl|}{\textbf {المواصفات}}&&{\textbf {التنفيذ}}\\\hline {\text{نوع البيانات المجرد}}&\xrightarrow {\text{تجسيد البيانات}} &{\text{بنية البيانات}}\\{\text{العمليات}}&{\xrightarrow[{\text{تحليل العمليات}}]{}}&{\text{الخوارزميات}}\end{array}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e7cfd927beebe328e3bd51537dffb7316579b2b7)
تجسيد البيانات
تتضمن عملية تجسيد البيانات (التحسين التدريجي) إيجاد تمثيل أكثر واقعية لأنواع البيانات المجردة المستخدمة في المواصفات. قد يتطلب الأمر عدة خطوات قبل الوصول إلى التنفيذ. 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. يجب إثبات أن العمليات والدوال الجديدة تحافظ على ثوابت أنواع البيانات في التمثيل الجديد. ولإثبات أن العمليات والدوال الجديدة تُحاكي تلك الموجودة في المواصفات الأصلية، يجب الوفاء بالتزامين من التزامات الإثبات:
- قاعدة النطاق:
forall r: NEW_REP & pre - OPA (retr(r)) => pre - OPR (r) - قاعدة النمذجة:
لكل ~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يتحقق من وجود عامل معين في المصنع أم لا
رسميًا، سيكون هذا كالتالي:
أنواع الشخص = رمز؛ العمال = مجموعة من الأشخاص ؛ولاية AWCCS التابعة للرئيس: نهاية العمالالعمليات INIT () ext wr pres: Workers post pres = {};أدخل (p : شخص ) ext wr pres : عمال pre p ليس في مجموعة 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].
تُعدّ طريقة فيينا للتطوير مفيدة للأنظمة القائمة على النماذج، لكنها غير مناسبة إذا كان النظام قائمًا على الزمن. في مثل هذه الحالات، يكون حساب التفاضل والتكامل للأنظمة المتصلة (CCS) أكثر فائدة.
انظر أيضاً
- الأساليب الرسمية
- المواصفات الرسمية
- لغة بيجين
- منطق المسند
- حساب القضايا
- لغة المواصفات Z ، البديل الرئيسي للغة VDM-SL (قارن)
للمزيد من القراءة
- بيورنر، داينز؛ كليف ب. جونز (1978). منهج فيينا للتطوير: اللغة الوصفية، سلسلة محاضرات في علوم الحاسوب 61. برلين، هايدلبرغ، نيويورك: سبرينغر. ISBN 978-0-387-08766-5.
- أوريغان، جيرارد (2006). المناهج الرياضية لجودة البرمجيات . لندن: سبرينغر. ISBN 978-1-84628-242-3.
- كليف ب. جونز (محرر). (1984). لغات البرمجة وتعريفها - هـ. بيكيتش (1936-1982) . سلسلة محاضرات في علوم الحاسوب . المجلد 177. برلين، هايدلبرغ، نيويورك، طوكيو: سبرينغر-فيرلاغ. doi : 10.1007/BFb0048933 . ISBN 978-3-540-13378-0. S2CID 7488558 .
- فيتزجيرالد، جيه إس ولارسون، بي جي، نمذجة الأنظمة: أدوات وتقنيات عملية في هندسة البرمجيات . مطبعة جامعة كامبريدج ، 1998. رقم ISBN 0-521-62348-0(حانة الطبعة اليابانية. إيوانامي شوتن 2003 ISBN 4-00-005609-3). [ 10 ]
- فيتزجيرالد، جيه إس ، ولارسون، بي جي، وموخرجي، بي، وبلات، إن، وفيرهوف، إم، تصاميم مُدققة لأنظمة كائنية التوجه . سبرينغر فيرلاغ 2005. ISBN 1-85233-881-4موقع ويب داعمتمت أرشفة هذا المحتوى في 2 مارس 2018 على موقع Wayback Machine، ويتضمن أمثلة ودعمًا مجانيًا للأدوات. [ 11 ]
- جونز، سي بي ، تطوير البرمجيات المنهجي باستخدام VDM ، برنتيس هول 1990. ISBN 0-13-880733-7متاح أيضًا عبر الإنترنت مجانًا: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip مؤرشف بتاريخ 17 يوليو 2011 في أرشيف الإنترنت (Wayback Machine)
- بيورنر، د. وجونز ، سي بي ، المواصفات الرسمية وتطوير البرمجيات ، برنتيس هول إنترناشونال، 1982. ISBN 0-13-880733-7
- جي دوز، الدليل المرجعي VDM-SL ، بيتمان 1991. ISBN 0-273-03151-1
- المنظمة الدولية للتوحيد القياسي ، تكنولوجيا المعلومات - لغات البرمجة وبيئاتها وواجهات برامج النظام - منهجية فيينا للتطوير - لغة المواصفات - الجزء 1: اللغة الأساسية المعيار الدولي ISO/IEC 13817-1، ديسمبر 1996.
- جونز، سي بي ، تطوير البرمجيات: منهج دقيق ، برنتيس هول إنترناشونال، 1980. رقم ISBN 0-13-821884-6
- جونز، سي بي وشاو، آر سي (محرران)، دراسات حالة في تطوير البرمجيات المنهجي ، برنتيس هول إنترناشونال، 1990. ISBN 0-13-880733-7
- بيكارغي، جيه سي، فيتزجيرالد، جيه إس ، ليندسي، بي إيه، مور، آر، وريتشي، بي، البرهان في VDM: دليل عملي . سبرينغر فيرلاغ، مناهج رسمية للحوسبة وتكنولوجيا المعلومات (FACIT)، 1994. ISBN 3-540-19813-X.
مراجع
- ↑ بعض الأفكار عن ذلك العمل، بما في ذلك التقرير الفني TR 25.139 بعنوان " تعريف رسمي لمجموعة فرعية من PL/1 "، بتاريخ 20 ديسمبر 1974، أعيد طبعه في جونز 1984، الصفحات 107-155. ومن الجدير بالذكر بشكل خاص قائمة المؤلفين بالترتيب: هـ. بيكيتش، د. بيورنر، و. هينهابل، سي. بي. جونز، ب. لوكاس.
- ↑ تم اعتماد علامة الجمع المزدوجة منلغة البرمجة الكائنية C++ المبنية على لغة C.
- ^ بيورنر وجونز 1978، المقدمة ، ص
- ↑ ملاحظات تمهيدية بقلم كليف ب. جونز (محرر) في بيكيتش 1984، ص. 7
- ^ بيورنر وجونز 1978، المقدمة ، ص.xi
- ^ بيورنر وجونز 1978، ص.24.
- ↑ انظر المقال الخاص بالاستمرارية لاستخدامه في علوم الحاسوب.
- ↑ كليمنسن، جيرت ب. (يناير 1986). "إعادة توجيه وإعادة استضافة نظام مُترجم DDC Ada: دراسة حالة - Honeywell DPS 6". رسائل ACM SIGAda Ada . 6 (1): 22-28 . doi : 10.1145/382256.382794 . S2CID 16337448 .
- ↑ بيتر غورم لارسن، "عشر سنوات من التطوير التاريخي لـ VDMTools" مؤرشف في 23 يناير 2021 في Wayback Machine ، في مجلة علوم الحاسوب العالمية ، المجلد 7 (8)، 2001
- ↑ " نمذجة الأنظمة: أدوات وتقنيات عملية في هندسة البرمجيات " . مؤرشف من الأصل في 17 مايو 2012. تم الاطلاع عليه في 8 سبتمبر 2007 .
- ↑ " تصاميم مُثبتة لأنظمة الكائنات الموجهة " . مؤرشف من الأصل في 2 مارس 2018. تم الاطلاع عليه في 8 سبتمبر 2007 .
روابط خارجية
- معلومات حول VDM و VDM++ (نسخة مؤرشفة على archive.org)
- لغة تعريف فيينا (VDL) مؤرشفة في 19 مايو 2009 على موقع Wayback Machine
- لغة نمذجة COMPASS مؤرشفة في 19 فبراير 2020 في Wayback Machine (CML)، وهي مزيج من VDM-SL مع CSP ، استنادًا إلى نظريات البرمجة الموحدة ، تم تطويرها لنمذجة أنظمة الأنظمة (SoS).
- الأساليب الرسمية
- لغات المواصفات الرسمية