فجوة المواصفات والتنفيذ: هنا تختبئ الأخطاء

يطرح أحد الادعاءات من حين لآخر في أوساط نظرية لغات البرمجة: «المواصفة المفصّلة بما يكفي لا تختلف عن الكود». الفكرة مثيرة للجدل، فهي تقول إن الفرق بين وصف ما يجب أن يفعله البرنامج وبين فعله فعلاً أضيق مما نظن. إذا كانت مواصفتك دقيقة إلى حد إزالة كل غموض، فأنت عملياً قد كتبت البرنامج.

هذا ليس مجرد فلسفة. فله آثار عملية على طريقة بناء البرمجيات، وعلى الدور الذي تلعبه المواصفات، ولماذا معظم الأخطاء ليست أخطاء برمجة بل فجوات في المواصفات. فهم المكان الذي تنتهي فيه المواصفات ويبدأ فيه التنفيذ يغيّر طريقة تفكيرك في الاختبار والأنواع والصحة.

أين تأتي معظم الأخطاء فعلاً

لو سألت مطوراً عن مصدر الأخطاء فغالباً سيقول: «الكود». لكن دراسات كثيرة عن عيوب البرمجيات تُظهر صورة مختلفة: معظم الأخطاء تنشأ في الفجوة بين النية والتنفيذ. الكود يفعل بالضبط ما أُمر به المطوّر، لكن الأمر نفسه كان خاطئاً لأن المواصفة، رسمية كانت أو غير رسمية، كانت غامضة أو ناقصة أو سُوء فهمها.

مثال كلاسيكي: تنص المواصفة على أن «النظام يجب أن يتعامل مع الطلبات المتزامنة». ماذا تعني «يتعامل»؟ هل تُعالَج بالترتيب؟ أم بالتوازي؟ أم تُوضع في طابور إذا كانت كثيرة؟ وما معنى «كثيرة»؟ وماذا يحدث للطلبات التي تصل والطابور ممتلئ؟ هذه ليست تفاصيل تنفيذ، بل فجوات في المواصفة. وكل سؤال بلا جواب هو خطأ محتمل، لأن المطوّر سيجيب عنه ضمنياً عبر التنفيذ، وقد لا تتطابق إجابته مع ما يتوقعه المستخدمون أو المطورون الآخرون.

طيف الدقة في المواصفات

تتدرج المواصفات من الوصف غير الرسمي إلى الصياغة الرسمية.

• لغة طبيعية. «يجب أن يكون نظام تسجيل الدخول آمناً وسهل الاستخدام.» هذه بالكاد مواصفة، بل أمنية. كل كلمة فيها غامضة. ما الذي يعنيه «آمن»؟ وما الذي يُعد «سهل الاستخدام»؟ هذه أحكام شخصية متنكرة في صورة متطلبات.
• لغة طبيعية منظّمة. «إذا أدخل المستخدم كلمة مرور خاطئة ثلاث مرات خلال 10 دقائق، يُقفل الحساب لمدة 30 دقيقة.» أدق، لكنها ما زالت غامضة. هل تشمل «كلمة المرور الخاطئة» الإرسال الفارغ؟ وهل يجب أن تكون المحاولات الثلاث متتالية؟ وهل نافذة الـ10 دقائق متحركة أم ثابتة؟
• توقيعات الأنواع. authenticate(username: string, password: string) -> Result<User, AuthError>. هذا يحدد واجهة الدالة بدقة، لكنه لا يقول شيئاً عن سلوكها. تعرف شكل المدخلات والمخرجات، لكنك لا تعرف العلاقة بينهما.
• مواصفات قائمة على الخصائص. «لكل زوج صالح من اسم المستخدم وكلمة المرور في قاعدة البيانات، تُرجع authenticate القيمة Ok(user) حيث user.username == username.» هذا يقيّد السلوك بدقة أكبر باستخدام المُسوِّرات المنطقية.
• مواصفة رسمية. نموذج رياضي كامل لسلوك النظام، يشمل كل حالة وكل انتقال وكل ثابت. عند هذا المستوى تكاد المواصفة والتنفيذ يصبحان الشيء نفسه.

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

الأنواع كمواصفات خفيفة

أنظمة الأنواع هي الشكل الأكثر انتشاراً للمواصفات في البرمجة اليومية. هي لا تصف السلوك، لكنها تقيّده. الدالة التي تُرجع Option<User> بدلاً من User تحدد أنها قد لا تجد مستخدماً، والمُترجم يُجبر كل مستدعٍ على التعامل مع هذا الاحتمال.

// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User  // What if ID is invalid?
//                                  // What if user not found?
//                                  // Does it panic? Return null?
//                                  // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.

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

الفكرة الجوهرية: كل تعليق نوعي هو مواصفة تُفحص تلقائياً. وكل سلوك تستطيع ترميزه في نظام الأنواع هو فئة من الأخطاء لن تواجهها أبداً.

اختبار قائم على الخصائص: تحديد السلوك

اختبارات الوحدة مواصفات قائمة على أمثلة: «بمدخل محدد، أتوقع مخرجاً محدداً». وهي مفيدة لكنها ناقصة بطبيعتها، لأنك لا تختبر إلا الحالات التي تفكر فيها. الاختبار القائم على الخصائص يقلب الفكرة: تحدد الخصائص التي يجب أن تتحقق لكل المدخلات، ويولّد إطار الاختبار مدخلات عشوائية للبحث عن انتهاكات.

from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.

الخصائص الثلاث في هذا الاختبار لا تختبر الترتيب فحسب، بل تُعرّفه. أي دالة تحقق الخصائص الثلاث هي، بالتعريف، فرز صحيح. هذه فكرة «المواصفة ككود» في أوضح صورها العملية: اكتب الخصائص التي تحدد السلوك الصحيح، ثم دع إطار الاختبار يتحقق من أن تنفيذك يلتزم بها.

TLA+ وفحص النماذج

للأنظمة التي تكون فيها الأخطاء مكلفة، كالأنظمة الموزعة والمنصات المالية والبنى التحتية الحرجة، توفر أدوات المواصفات الرسمية مثل TLA+ ضمانات أقوى. يتيح TLA+ (Temporal Logic of Actions) وصف سلوك النظام كآلة حالات، ثم فحصه نموذجياً عبر استكشاف كل التنفيذات الممكنة للتحقق من بقاء الثوابت صحيحة.

استخدمت Amazon نظام TLA+ للتحقق من خوارزميات في S3 وDynamoDB وخدمات AWS الحرجة الأخرى. وقد وصفت علناً أخطاء وجدتها كان من شبه المستحيل اكتشافها بالاختبار، أخطاء لا تظهر إلا في ترتيبات معينة للعمليات المتزامنة قد تحدث مرة واحدة من بين ملايين التنفيذات.

مواصفة TLA+ لبروتوكول توافق مثل Raft تكون عادةً بضع مئات من الأسطر. وهي تصف كل انتقال حالة مسموح، وكل ثابت (مثلاً «قائد واحد على الأكثر في كل فترة حكم»)، وكل خاصية أمان. ثم يستكشف فاحص النماذج مليارات مسارات التنفيذ المحتملة، ويتحقق من أن أياً منها لا ينتهك أي ثابت. هذه مواصفة قريبة فعلاً من الكود، دقيقة لدرجة أنك تستطيع ترجمتها آلياً إلى تنفيذ.

التصميم بالعقود

يقع التصميم بالعقود (Design by Contract) لبيرتراند ماير في منطقة وسطى عملية. كل دالة تحدد شروطاً مسبقة (ما يجب أن يكون صحيحاً قبل استدعاء الدالة)، وشروطاً لاحقة (ما تضمنه الدالة عند عودتها)، وثوابت (ما يجب أن يبقى صحيحاً دائماً للكائن). تُفحص هذه العقود أثناء التشغيل في مرحلة التطوير، ويمكن تعطيلها في الإنتاج لتحسين الأداء.

def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount

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

توصيات عملية

المواصفات الرسمية الكاملة ليست عملية لمعظم البرمجيات. لكن يمكنك تضييق فجوة المواصفات بدرجة كبيرة باستخدام تقنيات تتناسب مع سير العمل الاعتيادي في التطوير.

1. استخدم نظام الأنواع بقوة. رمّز القيود في الأنواع كلما أمكن. فضّل NonEmptyList على List حين لا ينبغي أن تكون القائمة فارغة. استخدم أغلفة newtype للتمييز بين UserId وOrderId رغم أن كليهما نص. كل قيد ترمّزه في الأنواع هو قيد يتحقق منه المُترجم دون تكلفة إضافية.
2. اكتب اختبارات قائمة على الخصائص للمنطق الأساسي. حدد الثوابت التي يجب أن يحافظ عليها نظامك وعبّر عنها كاختبارات خصائص. حتى عدد قليل من الخصائص المختارة بعناية يلتقط أخطاء تفوتها آلاف الاختبارات القائمة على الأمثلة.
3. حدّد الحدود. أهم المواصفات تقع عند حدود النظام: عقود الواجهات البرمجية (API)، ومخططات قواعد البيانات، وصيغ الرسائل. استخدم مواصفات OpenAPI أو Protocol Buffers أو JSON Schema لجعلها قابلة للفحص آلياً.
4. استخدم TLA+ أو Alloy للأنظمة المتزامنة الحرجة. إذا كنت تصمم خوارزمية توافق أو قفلاً موزعاً أو نظام معاملات مالية، فتكلفة المواصفة الرسمية صغيرة مقارنة بتكلفة أخطاء الصحة الدقيقة في الإنتاج.
5. اكتب المواصفة قبل الاختبارات. إذا لم تستطع أن تصوغ بدقة كيف يبدو السلوك الصحيح، فلن تستطيع التحقق منه. قضاء 30 دقيقة في كتابة مواصفة واضحة لما ينبغي أن تفعله دالة ما (كل الحالات بما فيها الحالات الطرفية) يكشف غالباً مشكلات في التصميم قبل كتابة سطر واحد من الكود.

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