باختصار
المواصفة الصورية (Formal Specification) وصف دقيق، بلغة رياضية لها قواعد ومعانٍ محدّدة، لما يجب أن يفعله نظام برمجي. وهي تصف «ماذا» يفعل النظام، لا «كيف» يفعله.
بالتفصيل
بحسب Wikipedia، تساعد المواصفات الصورية على وصف النظام وتحليل سلوكه، وعلى تصميمه بالتحقّق من خصائصه المهمّة بأدوات استدلال صارمة. ومع وجود مواصفة كهذه يمكن استخدام التحقّق الصوري لإثبات أن التصميم صحيح بالنسبة إليها، قبل استثمار كبير في التنفيذ.
والنقطة الجوهرية أن البرنامج لا يمكن أن يُوصف بأنه «صحيح» وحده، بل «صحيح بالنسبة إلى مواصفة محدّدة». أما هل تصف المواصفة المشكلة الحقيقية بدقّة، فهذه مسألة منفصلة وصعبة، لأنها تتطلّب تحويل مشكلة غير رسمية من العالم الحقيقي إلى تمثيل رياضي، وهذه الخطوة نفسها لا يمكن إثباتها رياضيًا.
وبحسب Wikipedia، من صفات المواصفة الجيدة أن تكون كافية، ومتّسقة داخليًا، وواضحة بلا لبس، وكاملة، وموجزة.
ومع دخول الذكاء الاصطناعي هذا المجال، صارت النماذج تساعد في كتابة المواصفات نفسها. فتنقل Wired مثالًا بسيطًا: مواصفة لجدول بيانات قد تشترط أن يحتوي العناصر نفسها قبل الترتيب وبعده، بترتيب مختلف فقط. ويحذّر بعض المختصّين من أن المواصفات المولّدة آليًا قد تمنح «ثقة غير مبرّرة».
مثال عملي
تطلب من خيّاط بدلة. الوصف العادي: «أريدها أنيقة ومريحة». المواصفة الصورية: طول الكمّ 62 سنتيمترًا، ومحيط الصدر 104، ولا تزيد المسافة بين الأزرار على 10 سنتيمترات. الوصف الأول يحتمل ألف بدلة، والثاني يمكن قياسه والتحقّق منه بشريط القياس.
لكن انتبه: إن أخطأت أنت في قياس ذراعك، ستخرج البدلة مطابقة للمواصفة تمامًا.. وضيّقة تمامًا.
مصطلحات مرتبطة
- Formal Verification — التحقّق الصوري.
- Proof Assistant — مساعد البرهان.
- Correctness — صحّة البرنامج.
- Specification Gaming — التلاعب بالمواصفات.
