هذه المقالة هي ترجمة . ولكن أمامها مقدمة صغيرة. كيف تتشكل الزومبي؟ دخل الجميع في موقف يريدون فيه جذب صديق أو زميل إلى مستواهم ، لكن هذا لا ينجح. ولا يتعلق الأمر معك بقدر ما هو "لا ينجح": في أحد جانبي الجدول يوجد راتب عادي ومهام وما إلى ذلك ، ومن ناحية أخرى ، الحاجة إلى التفكير. التفكير مزعج ومؤلم. سرعان ما يستسلم ويستمر في كتابة التعليمات البرمجية دون تشغيل دماغه على الإطلاق. تتخيل مقدار الجهد المطلوب للتغلب على حاجز العجز المكتسب ، وأنت لا تفعل ذلك. هذه هي الطريقة التي تتشكل بها الزومبي ، والتي ، على ما يبدو ، يمكن علاجها ، لكن يبدو أن لا أحد سيفعل ذلك.
عندما رأيت ذلك (نعم ، نفس الرفيق من الكتب المدرسية) ولا أقدم تقريرًا ، لكن جلسة أسئلة وأجوبة ، كنت حذرة بعض الشيء. فقط في حالة ، ليزلي هو عالم مشهور عالميًا ، ومؤلف الأعمال الأساسية في الحوسبة الموزعة ، ويمكنك أيضًا التعرف عليه من خلال الأحرف La في كلمة LaTeX - "Lamport TeX". العامل الثاني المثير للقلق هو مطلبه: يجب على كل شخص يأتي (مجانًا تمامًا) الاستماع إلى تقريرين من تقاريره مقدمًا ، وطرح سؤال واحد على الأقل بشأنها ، وبعد ذلك فقط يأتي. قررت أن أرى ما يبثه لامبورت هناك - وهذا رائع! إنه بالضبط ذلك الشيء ، الحبة السحرية لعلاج الزومبي. أحذرك: من النص ، يمكن لعشاق المنهجيات فائقة المرونة وأولئك الذين لا يحبون اختبار ما هو مكتوب أن ينفدوا بشكل ملحوظ.
بعد الهبروكات ، في الواقع ، تبدأ ترجمة الندوة. استمتع بالقراءة!
مهما كانت المهمة التي تقوم بها ، فأنت بحاجة دائمًا إلى اتباع ثلاث خطوات:
- حدد الهدف الذي تريد تحقيقه ؛
- تقرر كيف ستحقق هدفك ؛
- تعال إلى هدفك.
هذا ينطبق أيضا على البرمجة. عندما نكتب رمزًا ، نحتاج إلى:
- تحديد ما يجب أن يفعله البرنامج ؛
- تحديد كيفية أداء مهمتها ؛
- اكتب الكود المقابل.
الخطوة الأخيرة ، بالطبع ، مهمة للغاية ، لكنني لن أتحدث عنها اليوم. بدلاً من ذلك ، سنناقش الأولين. يقوم كل مبرمج بتنفيذها قبل البدء في العمل. لا تجلس لتكتب إلا إذا قررت ما إذا كنت تكتب متصفحًا أو قاعدة بيانات. يجب أن تكون فكرة معينة عن الهدف موجودة. وأنت بالتأكيد تفكر في ما سيفعله البرنامج بالضبط ، ولا تكتب بطريقة ما على أمل أن تتحول الشفرة بطريقة ما إلى متصفح.
كيف يحدث هذا التفكير المسبق بالضبط؟ ما مقدار الجهد الذي يجب أن نبذله في هذا؟ كل هذا يتوقف على مدى تعقيد المشكلة التي نحلها. لنفترض أننا نريد كتابة نظام توزيع متسامح مع الخطأ. في هذه الحالة ، يجب أن نفكر في الأمور بعناية قبل أن نجلس على الكود. ماذا لو احتجنا فقط إلى زيادة متغير عدد صحيح بمقدار 1؟ للوهلة الأولى ، كل شيء تافه هنا ، ولا داعي للتفكير ، ولكن بعد ذلك نتذكر أنه يمكن حدوث فيضان. لذلك ، حتى لفهم ما إذا كانت المشكلة بسيطة أم معقدة ، عليك أولاً التفكير.
إذا كنت تفكر في الحلول الممكنة للمشكلة مسبقًا ، يمكنك تجنب الأخطاء. لكن هذا يتطلب أن يكون تفكيرك واضحًا. لتحقيق ذلك ، تحتاج إلى تدوين أفكارك. أحب حقًا اقتباس ديك جويندون: "عندما تكتب ، تُظهر لك الطبيعة كيف يكون تفكيرك قذرًا." إذا لم تكتب ، فأنت تعتقد فقط أنك تفكر. وتحتاج إلى تدوين أفكارك في شكل مواصفات.
المواصفات تؤدي وظائف عديدة ، خاصة في المشاريع الكبيرة. لكنني سأتحدث فقط عن واحد منهم: إنهم يساعدوننا على التفكير بوضوح. من الواضح أن التفكير مهم جدًا وصعب للغاية ، لذلك نحن بحاجة إلى أي مساعدة. بأي لغة يجب أن نكتب المواصفات؟ بشكل عام ، هذا هو السؤال الأول دائمًا للمبرمجين: ما هي اللغة التي سنكتب بها. لا توجد إجابة واحدة صحيحة لها: المشاكل التي نحلها متنوعة للغاية. بالنسبة للبعض ، TLA + هي لغة مواصفات قمت بتطويرها. بالنسبة للآخرين ، من الأنسب استخدام اللغة الصينية. كل شيء يعتمد على الموقف.
والأهم هو سؤال آخر: كيف نحقق تفكيرًا أوضح؟ الجواب: يجب أن نفكر مثل العلماء. هذه طريقة في التفكير أثبتت نفسها على مدى 500 عام الماضية. في العلم ، نبني نماذج رياضية للواقع. ربما كان علم الفلك هو العلم الأول بالمعنى الدقيق للكلمة. في النموذج الرياضي المستخدم في علم الفلك ، تظهر الأجرام السماوية كنقاط ذات كتلة وموضع وزخم ، على الرغم من أنها في الواقع كائنات معقدة للغاية مع الجبال والمحيطات والمد والجزر. تم إنشاء هذا النموذج ، مثل أي نموذج آخر ، لحل مشاكل معينة. إنه أمر رائع لتحديد مكان توجيه التلسكوب إذا كنت بحاجة إلى العثور على كوكب. لكن إذا كنت تريد التنبؤ بالطقس على هذا الكوكب ، فلن يعمل هذا النموذج.
تسمح لنا الرياضيات بتحديد خصائص النموذج. ويوضح العلم كيف ترتبط هذه الخصائص بالواقع. لنتحدث عن علومنا وعلوم الكمبيوتر. الواقع الذي نعمل به هو أنظمة الحوسبة بمختلف أنواعها: المعالجات ووحدات التحكم في الألعاب وأجهزة الكمبيوتر وبرامج التنفيذ وما إلى ذلك. سأتحدث عن تشغيل برنامج على جهاز كمبيوتر ، ولكن بشكل عام ، تنطبق كل هذه الاستنتاجات على أي نظام كمبيوتر. في علمنا ، نستخدم العديد من النماذج المختلفة: آلة تورينج ، ومجموعات الأحداث المرتبة جزئيًا ، والعديد من النماذج الأخرى.
ما هو البرنامج؟ هذا هو أي رمز يمكن اعتباره بشكل مستقل. افترض أننا بحاجة إلى كتابة متصفح. نقوم بثلاث مهام: نصمم عرض المستخدم للبرنامج ، ثم نكتب الرسم التخطيطي عالي المستوى للبرنامج ، وأخيرًا نكتب الكود. أثناء كتابة الكود ، ندرك أننا بحاجة إلى كتابة منسق نص. نحتاج هنا مرة أخرى إلى حل ثلاث مشاكل: تحديد النص الذي ستعود إليه هذه الأداة ؛ حدد خوارزمية للتنسيق ؛ اكتب كود. هذه المهمة لها مهمة فرعية خاصة بها: أدخل واصلة بشكل صحيح في الكلمات. نقوم أيضًا بحل هذه المهمة الفرعية في ثلاث خطوات - كما ترى ، يتم تكرارها على عدة مستويات.
دعنا نفكر بمزيد من التفصيل في الخطوة الأولى: ما هي المشكلة التي يحلها البرنامج. هنا ، غالبًا ما نقوم بنمذجة برنامج كدالة تأخذ بعض المدخلات وتنتج بعض المخرجات. في الرياضيات ، توصف الوظيفة عادةً على أنها مجموعة مرتبة من الأزواج. على سبيل المثال ، يتم وصف دالة التربيع للأعداد الطبيعية بالمجموعة {<0,0،1,1>، <2,4،3,9>، <XNUMX،XNUMX>، <XNUMX،XNUMX>،…}. مجال هذه الوظيفة هو مجموعة العناصر الأولى لكل زوج ، أي الأعداد الطبيعية. لتحديد دالة ، نحتاج إلى تحديد نطاقها وصيغتها.
لكن الوظائف في الرياضيات ليست مثل الوظائف في لغات البرمجة. الرياضيات أسهل بكثير. بما أنه ليس لدي وقت لأمثلة معقدة ، فلنأخذ مثالًا بسيطًا: دالة في C أو طريقة ثابتة في Java تُرجع القاسم المشترك الأكبر لعددين صحيحين. في مواصفات هذه الطريقة ، سنكتب: يحسب GCD(M,N) للحجج M и Nحيث GCD(M,N) - دالة مجالها هو مجموعة أزواج الأعداد الصحيحة ، والقيمة المعادة هي أكبر عدد صحيح يقبل القسمة على M и N. كيف يرتبط هذا النموذج بالواقع؟ يعمل النموذج على أعداد صحيحة ، بينما في C أو Java لدينا 32 بت int. يتيح لنا هذا النموذج تحديد ما إذا كانت الخوارزمية صحيحة GCD، لكنها لن تمنع أخطاء تجاوز السعة. سيتطلب هذا نموذجًا أكثر تعقيدًا ، لا يوجد وقت له.
دعنا نتحدث عن حدود الوظيفة كنموذج. بعض البرامج (مثل أنظمة التشغيل) لا تقوم فقط بإرجاع قيمة معينة لوسائط معينة ، بل يمكنها العمل بشكل مستمر. بالإضافة إلى ذلك ، فإن الوظيفة كنموذج ليست مناسبة تمامًا للخطوة الثانية: التخطيط لكيفية حل المشكلة. يحسب الفرز السريع والفرز الفقاعي نفس الوظيفة ، لكنهما خوارزميات مختلفة تمامًا. لذلك ، لوصف كيفية تحقيق هدف البرنامج ، أستخدم نموذجًا مختلفًا ، دعنا نسميه النموذج السلوكي القياسي. يتم تمثيل البرنامج الموجود فيه كمجموعة من جميع السلوكيات المسموح بها ، وكل منها بدورها عبارة عن سلسلة من الحالات ، والحالة هي تخصيص القيم للمتغيرات.
دعونا نرى كيف ستبدو الخطوة الثانية لخوارزمية إقليدس. نحن بحاجة إلى الحساب GCD(M, N). نحن نبدأ M كيف xو N كيف y، ثم اطرح بشكل متكرر أصغر هذه المتغيرات من الأكبر حتى تتساوى. على سبيل المثال ، إذا M = 12و N = 18يمكننا وصف السلوك التالي:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A ما لم M = 0 и N = 0؟ الصفر قابل للقسمة على جميع الأعداد ، لذلك لا يوجد قاسم أكبر في هذه الحالة. في هذه الحالة ، نحتاج إلى العودة إلى الخطوة الأولى ونسأل: هل نحتاج حقًا إلى حساب GCD للأرقام غير الموجبة؟ إذا لم يكن ذلك ضروريًا ، فأنت تحتاج فقط إلى تغيير المواصفات.
هنا يجب أن نقوم باستطراد بسيط حول الإنتاجية. غالبًا ما يتم قياسه بعدد سطور التعليمات البرمجية المكتوبة يوميًا. لكن عملك يكون أكثر فائدة إذا تخلصت من عدد معين من السطور ، لأن لديك مساحة أقل للأخطاء. أسهل طريقة للتخلص من الكود هي الخطوة الأولى. من المحتمل تمامًا أنك لست بحاجة إلى كل الأجراس والصفارات التي تحاول تنفيذها. أسرع طريقة لتبسيط البرنامج وتوفير الوقت هي عدم القيام بأشياء لا ينبغي القيام بها. الخطوة الثانية هي ثاني أكثر احتمالية لتوفير الوقت. إذا كنت تقيس الإنتاجية من حيث الأسطر المكتوبة ، فإن التفكير في كيفية إنجاز مهمة ما سوف يجعلك أقل إنتاجية، لأنه يمكنك حل نفس المشكلة برمز أقل. لا يمكنني تقديم إحصائيات دقيقة هنا ، لأنه ليس لدي طريقة لحساب عدد الأسطر التي لم أكتبها بسبب حقيقة أنني أمضيت وقتًا في المواصفات ، أي في الخطوتين الأولى والثانية. ولا يمكن إجراء التجربة هنا أيضًا ، لأنه في التجربة ليس لدينا الحق في إكمال الخطوة الأولى ، والمهمة محددة مسبقًا.
من السهل التغاضي عن العديد من الصعوبات في المواصفات غير الرسمية. لا يوجد شيء صعب في كتابة المواصفات الصارمة للوظائف ، ولن أناقش هذا. بدلاً من ذلك ، سنتحدث عن كتابة مواصفات قوية للسلوكيات القياسية. هناك نظرية تنص على أنه يمكن وصف أي مجموعة من السلوكيات باستخدام خاصية الأمان (سلامة) وخصائص البقاء (الحياة). الأمان يعني أنه لن يحدث شيء سيء ، فلن يعطي البرنامج إجابة غير صحيحة. البقاء على قيد الحياة يعني أن شيئًا جيدًا سيحدث عاجلاً أم آجلاً ، أي أن البرنامج سيعطي الإجابة الصحيحة عاجلاً أم آجلاً. كقاعدة عامة ، يعد الأمان مؤشرًا أكثر أهمية ، وغالبًا ما تحدث الأخطاء هنا. لذلك ، لتوفير الوقت ، لن أتحدث عن البقاء على قيد الحياة ، رغم أنه بالطبع مهم أيضًا.
نحقق الأمن من خلال تحديد مجموعة الحالات الأولية المحتملة أولاً. وثانيًا ، العلاقات مع جميع الدول التالية المحتملة لكل ولاية. دعونا نتصرف مثل العلماء ونحدد الدول رياضيا. يتم وصف مجموعة الحالات الأولية بواسطة صيغة ، على سبيل المثال ، في حالة خوارزمية إقليدس: (x = M) ∧ (y = N). لقيم معينة M и N هناك حالة ابتدائية واحدة فقط. يتم وصف العلاقة مع الحالة التالية بواسطة صيغة يتم فيها كتابة متغيرات الحالة التالية برقم أولي ، ومتغيرات الحالة الحالية مكتوبة بدون رئيس. في حالة خوارزمية إقليدس ، سنتعامل مع فصل صيغتين ، في إحداها x هي القيمة الأكبر ، وفي الثانية - y:
في الحالة الأولى ، القيمة الجديدة لـ y تساوي القيمة السابقة لـ y ، ونحصل على القيمة الجديدة لـ x بطرح المتغير الأصغر من المتغير الأكبر. في الحالة الثانية ، نفعل العكس.
دعنا نعود إلى خوارزمية إقليدس. لنفترض ذلك مرة أخرى M = 12, N = 18. هذا يحدد حالة أولية واحدة ، (x = 12) ∧ (y = 18). ثم نعوض بهذه القيم في الصيغة أعلاه ونحصل على:
إليك الحل الوحيد الممكن: x' = 18 - 12 ∧ y' = 12ونحصل على السلوك: [x = 12, y = 18]. وبالمثل ، يمكننا وصف جميع الحالات في سلوكنا: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
في آخر دولة [x = 6, y = 6] سيكون كلا الجزأين من التعبير خاطئين ، لذلك ليس له الحالة التالية. لذا ، لدينا مواصفات كاملة للخطوة الثانية - كما ترون ، هذه رياضيات عادية تمامًا ، كما هو الحال في المهندسين والعلماء ، وليست غريبة ، كما هو الحال في علوم الكمبيوتر.
يمكن دمج هاتين الصيغتين في صيغة واحدة للمنطق الزمني. إنها أنيقة وسهلة الشرح ، لكن لا يوجد وقت لها الآن. قد نحتاج إلى منطق زمني فقط لخاصية الحيوية ، فهو ليس ضروريًا للأمان. أنا لا أحب المنطق الزمني على هذا النحو ، فهو ليس رياضيات عادية تمامًا ، لكن في حالة الحيوية ، فهو شر لا بد منه.
في خوارزمية إقليدس ، لكل قيمة x и y لها قيم فريدة x' и y'، مما يجعل العلاقة مع الحالة التالية صحيحة. بعبارة أخرى ، خوارزمية إقليدس حتمية. لنمذجة خوارزمية غير حتمية ، تحتاج الحالة الحالية إلى حالات مستقبلية متعددة محتملة ، وأن كل قيمة متغيرة غير محددة لها قيم متغيرة معدة متعددة بحيث تكون العلاقة مع الحالة التالية صحيحة. من السهل القيام بذلك ، لكنني لن أعطي أمثلة الآن.
لصنع أداة عمل ، تحتاج إلى رياضيات رسمية. كيف تجعل المواصفات رسمية؟ للقيام بذلك ، نحتاج إلى لغة رسمية ، على سبيل المثال ، . ستبدو مواصفات خوارزمية إقليدس كما يلي في هذه اللغة:
رمز علامة التساوي مع المثلث يعني أن القيمة الموجودة على يسار الإشارة معرّفة لتكون مساوية للقيمة الموجودة على يمين العلامة. في جوهرها ، المواصفات هي تعريف ، في حالتنا تعريفين. بالنسبة للمواصفات في TLA + ، تحتاج إلى إضافة بعض التصريحات وبعض الصياغة ، كما في الشريحة أعلاه. في ASCII سيبدو كما يلي:
كما ترون ، لا شيء معقد. يمكن اختبار مواصفات TLA + ، أي تجاوز جميع السلوكيات الممكنة في نموذج صغير. في حالتنا ، سيكون هذا النموذج قيمًا معينة M и N. هذه طريقة تحقق فعالة وبسيطة للغاية وهي تلقائية تمامًا. من الممكن أيضًا كتابة براهين رسمية للحقيقة والتحقق منها ميكانيكيًا ، لكن هذا يستغرق الكثير من الوقت ، لذلك لا أحد يفعل ذلك تقريبًا.
العيب الرئيسي لـ TLA + هو أنها الرياضيات ، والمبرمجون وعلماء الكمبيوتر يخافون من الرياضيات. للوهلة الأولى ، هذا يبدو وكأنه مزحة ، لكن للأسف أعني ذلك بكل جدية. كان زميلي يخبرني للتو كيف حاول شرح TLA + للعديد من المطورين. بمجرد ظهور الصيغ على الشاشة ، أصبحت على الفور عيون زجاجية. لذلك إذا أخافتك TLA + ، يمكنك استخدام ، إنها نوع من لغة برمجة الألعاب. يمكن أن يكون التعبير في PlusCal أي تعبير TLA + ، أي بشكل عام أي تعبير رياضي. بالإضافة إلى ذلك ، يحتوي PlusCal على بناء جملة للخوارزميات غير الحتمية. نظرًا لأن PlusCal يمكنه كتابة أي تعبير TLA + ، فإن PlusCal أكثر تعبيرًا من أي لغة برمجة حقيقية. بعد ذلك ، يتم تجميع PlusCal في مواصفات TLA + سهلة القراءة. هذا لا يعني ، بالطبع ، أن مواصفات PlusCal المعقدة ستتحول إلى مواصفات بسيطة على TLA + - فقط المراسلات بينهما واضحة ، ولن يكون هناك تعقيد إضافي. أخيرًا ، يمكن التحقق من هذه المواصفات بواسطة أدوات TLA +. الكل في الكل ، يمكن أن يساعد PlusCal في التغلب على الرهاب الرياضي ويسهل فهمه حتى بالنسبة للمبرمجين وعلماء الكمبيوتر. في الماضي ، قمت بنشر الخوارزميات عليها لبعض الوقت (حوالي 10 سنوات).
ربما يعترض شخص ما على أن TLA + و PlusCal هي رياضيات ، والرياضيات تعمل فقط على الأمثلة المخترعة. في الممارسة العملية ، أنت بحاجة إلى لغة حقيقية تحتوي على أنواع وإجراءات وعناصر وما إلى ذلك. هذا خطأ. هذا ما كتبه كريس نيوكومب ، الذي عمل في أمازون: "لقد استخدمنا TLA + في عشرة مشاريع كبرى ، وفي كل حالة أحدثت فرقًا كبيرًا في التطوير لأننا كنا قادرين على اكتشاف الأخطاء الخطيرة قبل أن نصل إلى مرحلة الإنتاج ، ولأنها أعطتنا البصيرة والثقة التي نحتاجها لتحقيق أداء قوي تحسينات دون التأثير على حقيقة البرنامج ". يمكنك في كثير من الأحيان أن تسمع أنه عند استخدام الأساليب الرسمية ، نحصل على كود غير فعال - من الناحية العملية ، كل شيء هو عكس ذلك تمامًا. بالإضافة إلى ذلك ، هناك رأي مفاده أنه لا يمكن إقناع المديرين بالحاجة إلى الأساليب الرسمية ، حتى لو اقتنع المبرمجون بفائدتها. وكتب نيوكومب: "يبذل المديرون الآن قصارى جهدهم لكتابة مواصفات TLA + ، ويخصصون وقتًا لذلك على وجه التحديد". لذلك عندما يرى المديرون أن TLA + تعمل ، يسعدهم قبولها. كتب كريس نيوكومب هذا منذ حوالي ستة أشهر (أكتوبر 2014) ، ولكن الآن ، على حد علمي ، يتم استخدام TLA + في 14 مشروعًا ، وليس 10. مثال آخر في تصميم XBox 360. جاء أحد المتدربين إلى Charles Thacker و كتب مواصفات لنظام الذاكرة. بفضل هذه المواصفات ، تم العثور على خطأ كان من الممكن أن يمر دون أن يلاحظه أحد ، وبسببه سيتعطل كل جهاز XBox 360 بعد أربع ساعات من الاستخدام. أكد مهندسو شركة IBM أن اختباراتهم لم تكن لتجد هذا الخطأ.
يمكنك قراءة المزيد عن TLA + على الإنترنت ، ولكن دعنا نتحدث الآن عن المواصفات غير الرسمية. نادرًا ما نضطر إلى كتابة برامج تحسب القاسم المشترك الأصغر وما شابه. كثيرًا ما نكتب برامج مثل أداة الطابعة الجميلة التي كتبتها لـ TLA +. بعد أبسط معالجة ، سيبدو كود TLA + كما يلي:
ولكن في المثال أعلاه ، أراد المستخدم على الأرجح محاذاة علامتي الربط والمساواة. لذلك سيبدو التنسيق الصحيح أكثر مثل هذا:
تأمل مثالاً آخر:
هنا ، على العكس من ذلك ، كانت محاذاة علامات المساواة والجمع والضرب في المصدر عشوائية ، لذا فإن أبسط معالجة كافية تمامًا. بشكل عام ، لا يوجد تعريف رياضي دقيق للتنسيق الصحيح ، لأن كلمة "صحيح" في هذه الحالة تعني "ما يريده المستخدم" ، ولا يمكن تحديد ذلك رياضيًا.
يبدو أنه إذا لم يكن لدينا تعريف للحقيقة ، فإن التحديد يكون عديم الفائدة. لكنها ليست كذلك. فقط لأننا لا نعرف ما يفترض أن يفعله البرنامج لا يعني أننا لسنا بحاجة إلى التفكير في كيفية عمله - بل على العكس ، علينا بذل المزيد من الجهد فيه. المواصفات مهمة بشكل خاص هنا. من المستحيل تحديد البرنامج الأمثل للطباعة المهيكلة ، لكن هذا لا يعني أننا يجب ألا نأخذه على الإطلاق ، وكتابة الكود كتيار للوعي ليس بالأمر الجيد. في النهاية ، كتبت تحديدًا لست قواعد مع التعريفات في شكل تعليقات في ملف جافا. فيما يلي مثال على إحدى القواعد: a left-comment token is LeftComment aligned with its covering token. هذه القاعدة مكتوبة ، هل نقول ، الإنجليزية الرياضية: LeftComment aligned, left-comment и covering token - مصطلحات مع تعاريف. هذه هي الطريقة التي يصف بها علماء الرياضيات الرياضيات: يكتبون تعريفات للمصطلحات والقواعد بناءً عليها. وتتمثل فائدة مثل هذه المواصفات في أن ستة قواعد يسهل فهمها وتصحيحها أكثر من 850 سطرًا من التعليمات البرمجية. يجب أن أقول إن كتابة هذه القواعد لم يكن سهلاً ، فقد استغرق الأمر وقتًا طويلاً لتصحيحها. لهذا الغرض على وجه الخصوص ، كتبت رمزًا أبلغ عن القاعدة التي تم استخدامها. بفضل حقيقة أنني اختبرت هذه القواعد الست في عدة أمثلة ، لم أضطر إلى تصحيح 850 سطرًا من التعليمات البرمجية ، واتضح أنه من السهل جدًا العثور على الأخطاء. جافا لديها أدوات رائعة لهذا الغرض. إذا كنت قد كتبت الكود للتو ، فسيستغرق الأمر وقتًا أطول بكثير ، وكان التنسيق سيصبح أقل جودة.
لماذا لا يمكن استخدام المواصفات الرسمية؟ من ناحية أخرى ، التنفيذ الصحيح ليس مهمًا للغاية هنا. لا بد أن المطبوعات الهيكلية لا ترضي أي شخص ، لذلك لم أضطر إلى جعلها تعمل بشكل صحيح في جميع المواقف الغريبة. والأهم من ذلك هو حقيقة أنه لم يكن لدي الأدوات الكافية. مدقق نموذج TLA + عديم الفائدة هنا ، لذلك سأضطر إلى كتابة الأمثلة يدويًا.
المواصفات المذكورة أعلاه لها ميزات مشتركة في جميع المواصفات. إنه مستوى أعلى من الرمز. يمكن تنفيذه بأي لغة. أي أدوات أو طرق غير مجدية لكتابتها. لن تساعدك أي دورة برمجة في كتابة هذه المواصفات. ولا توجد أدوات يمكن أن تجعل هذه المواصفات غير ضرورية ، ما لم تكن ، بالطبع ، تكتب لغة خاصة لكتابة برامج طباعة منظمة في TLA +. أخيرًا ، لا تشير هذه المواصفات إلى أي شيء حول كيفية كتابة الكود بالضبط ، بل توضح فقط ما يفعله الكود. نكتب المواصفات لمساعدتنا على التفكير في المشكلة قبل أن نبدأ في التفكير في الكود.
لكن هذه المواصفات لها أيضًا ميزات تميزها عن المواصفات الأخرى. 95٪ من المواصفات الأخرى أقصر وأبسط بشكل ملحوظ:
علاوة على ذلك ، هذه المواصفات هي مجموعة من القواعد. كقاعدة عامة ، هذه علامة على ضعف المواصفات. إن فهم عواقب مجموعة من القواعد أمر صعب للغاية ، ولهذا السبب اضطررت إلى قضاء الكثير من الوقت في تصحيحها. ومع ذلك ، في هذه الحالة ، لم أجد طريقة أفضل.
يجدر قول بضع كلمات عن البرامج التي تعمل بشكل مستمر. كقاعدة عامة ، يعملون بالتوازي ، على سبيل المثال ، أنظمة التشغيل أو الأنظمة الموزعة. قلة قليلة من الناس يستطيعون فهمها عقليًا أو على الورق ، وأنا لست واحدًا منهم ، على الرغم من أنني كنت قادرًا على فعل ذلك مرة واحدة. لذلك ، نحتاج إلى أدوات ستتحقق من عملنا - على سبيل المثال ، TLA + أو PlusCal.
لماذا كان من الضروري كتابة المواصفات إذا كنت أعرف بالفعل ما يجب أن تفعله الشفرة بالضبط؟ في الحقيقة ، لقد ظننت أنني أعرف ذلك. بالإضافة إلى ذلك ، مع المواصفات ، لم يعد الشخص الخارجي بحاجة إلى الدخول في الكود لفهم ما يفعله بالضبط. لدي قاعدة: لا يجب أن تكون هناك قواعد عامة. هناك استثناء لهذه القاعدة ، بالطبع ، إنها القاعدة العامة الوحيدة التي أتبعها: تحديد ما يفعله الكود يجب أن يخبر الناس بكل ما يحتاجون إلى معرفته عند استخدام الكود.
إذن ما الذي يحتاج المبرمجون إلى معرفته بالضبط عن التفكير؟ بالنسبة للمبتدئين ، مثل أي شخص آخر: إذا لم تكتب ، فسيبدو لك فقط أنك تفكر. أيضًا ، عليك التفكير قبل كتابة التعليمات البرمجية ، مما يعني أنك بحاجة إلى الكتابة قبل كتابة التعليمات البرمجية. المواصفات هي ما نكتبه قبل أن نبدأ في الترميز. مطلوب مواصفات لأي كود يمكن استخدامه أو تعديله من قبل أي شخص. وقد يكون هذا "الشخص" هو نفسه مؤلف الشفرة بعد شهر من كتابتها. المواصفات مطلوبة للبرامج والأنظمة الكبيرة ، للفئات ، للطرق ، وأحيانًا حتى للأقسام المعقدة من طريقة واحدة. ما الذي يجب أن يكتب بالضبط عن الكود؟ تحتاج إلى وصف ما يفعله ، أي ما يمكن أن يكون مفيدًا لأي شخص يستخدم هذا الرمز. في بعض الأحيان قد يكون من الضروري أيضًا تحديد كيفية تحقيق الكود لغرضه. إذا مررنا بهذه الطريقة في سياق الخوارزميات ، فإننا نسميها خوارزمية. إذا كان شيئًا خاصًا وجديدًا ، فإننا نسميه التصميم عالي المستوى. لا يوجد فرق رسمي هنا: كلاهما نموذج مجرد لبرنامج.
كيف بالضبط يجب أن تكتب مواصفات الكود؟ الشيء الرئيسي: يجب أن يكون أعلى بمستوى واحد من الكود نفسه. يجب أن تصف الحالات والسلوكيات. يجب أن تكون صارمة كما تتطلب المهمة. إذا كنت تكتب تحديدًا لكيفية تنفيذ المهمة ، فيمكنك كتابتها بالرمز الزائف أو باستخدام PlusCal. تحتاج إلى تعلم كيفية كتابة المواصفات على المواصفات الرسمية. سيعطيك هذا المهارات اللازمة التي ستساعدك في المهارات غير الرسمية أيضًا. كيف تتعلم كتابة المواصفات الرسمية؟ عندما تعلمنا البرمجة ، كتبنا برامج ثم قمنا بتصحيحها. الأمر نفسه هنا: اكتب المواصفات ، وتحقق من ذلك باستخدام مدقق النموذج ، وأصلح الأخطاء. قد لا تكون TLA + هي أفضل لغة لمواصفات رسمية ، ومن المحتمل أن تكون لغة أخرى أفضل لاحتياجاتك الخاصة. تتمثل ميزة TLA + في أنها تعلم التفكير الرياضي جيدًا.
كيفية ربط المواصفات والكود؟ بمساعدة التعليقات التي تربط المفاهيم الرياضية وتنفيذها. إذا كنت تعمل مع الرسوم البيانية ، فعندئذ على مستوى البرنامج سيكون لديك مصفوفات من العقد ومصفوفات الروابط. لذلك ، عليك أن تكتب بالضبط كيف يتم تنفيذ الرسم البياني بواسطة هياكل البرمجة هذه.
وتجدر الإشارة إلى أنه لا ينطبق أي مما سبق على العملية الفعلية لكتابة الكود. عندما تكتب الكود ، أي أنك تقوم بالخطوة الثالثة ، تحتاج أيضًا إلى التفكير والتفكير في البرنامج. إذا تبين أن المهمة الفرعية معقدة أو غير واضحة ، فأنت بحاجة إلى كتابة مواصفات لها. لكنني لا أتحدث عن الكود نفسه هنا. يمكنك استخدام أي لغة برمجة ، أي منهجية ، فالأمر لا يتعلق بها. أيضًا ، لا يلغي أي مما سبق الحاجة إلى اختبار التعليمات البرمجية وتصحيحها. حتى لو تمت كتابة النموذج المجرد بشكل صحيح ، فقد تكون هناك أخطاء في تنفيذه.
مواصفات الكتابة هي خطوة إضافية في عملية الترميز. بفضله ، يمكن اكتشاف العديد من الأخطاء بجهد أقل - نحن نعرف ذلك من تجربة المبرمجين من Amazon. مع المواصفات ، تصبح جودة البرامج أعلى. فلماذا إذن نذهب في كثير من الأحيان بدونهم؟ لأن الكتابة صعبة. والكتابة صعبة ، لأن هذا يحتاج إلى التفكير ، والتفكير صعب أيضًا. من الأسهل دائمًا التظاهر بما تعتقده. هنا يمكنك رسم تشبيه مع الجري - فكلما ركضت أقل ، كلما ركضت بشكل أبطأ. تحتاج إلى تدريب عضلاتك وممارسة الكتابة. تحتاج إلى ممارسة.
قد تكون المواصفات غير صحيحة. ربما تكون قد ارتكبت خطأ في مكان ما ، أو ربما تكون المتطلبات قد تغيرت ، أو قد يلزم إجراء تحسين. يجب تغيير أي رمز يستخدمه أي شخص ، لذلك عاجلاً أم آجلاً لن تتطابق المواصفات مع البرنامج. من الناحية المثالية ، في هذه الحالة ، تحتاج إلى كتابة مواصفة جديدة وإعادة كتابة الكود بالكامل. نحن نعلم جيدًا أنه لا أحد يفعل ذلك. في الممارسة العملية ، نقوم بتصحيح الكود وربما نقوم بتحديث المواصفات. إذا كان هذا سيحدث عاجلاً أم آجلاً ، فلماذا تكتب المواصفات على الإطلاق؟ أولاً ، بالنسبة إلى الشخص الذي سيقوم بتحرير الكود الخاص بك ، فإن كل كلمة إضافية في المواصفات تستحق وزنها ذهباً ، وقد يكون هذا الشخص أنت نفسك. غالبًا ما أوبخ نفسي لعدم الحصول على مواصفات كافية عندما أقوم بتحرير الكود الخاص بي. وأنا أكتب مواصفات أكثر من الكود. لذلك ، عندما تقوم بتحرير الكود ، يجب تحديث المواصفات دائمًا. ثانيًا ، مع كل مراجعة ، تزداد الشفرة سوءًا ، وتصبح قراءتها وصيانتها أكثر صعوبة. هذه زيادة في الإنتروبيا. ولكن إذا لم تبدأ بمواصفات ، فسيكون كل سطر تكتبه بمثابة تعديل ، وستكون الشفرة غير عملية ويصعب قراءتها من البداية.
كما قيل , لم يتم كسب معركة بالخطة ، ولم يتم كسب معركة بدون خطة. وكان يعرف شيئًا أو شيئين عن المعارك. هناك رأي مفاده أن مواصفات الكتابة مضيعة للوقت. أحيانًا يكون هذا صحيحًا ، والمهمة بسيطة جدًا بحيث لا يوجد شيء للتفكير فيها. لكن يجب أن تتذكر دائمًا أنه عندما يُطلب منك عدم كتابة المواصفات ، يُطلب منك عدم التفكير. ويجب أن تفكر في الأمر في كل مرة. لا يضمن التفكير في المهمة أنك لن ترتكب أخطاء. كما نعلم ، لم يخترع أحد العصا السحرية ، والبرمجة مهمة صعبة. ولكن إذا لم تفكر في المشكلة ، فمن المضمون ارتكابك للأخطاء.
يمكنك قراءة المزيد حول TLA + و PlusCal على موقع ويب خاص ، يمكنك الانتقال إلى هناك من صفحتي الرئيسية . هذا كل شيء بالنسبة لي ، أشكركم على اهتمامكم.
يرجى ملاحظة أن هذه ترجمة. عندما تكتب تعليقات ، تذكر أن المؤلف لن يقرأها. إذا كنت تريد حقًا الدردشة مع المؤلف ، فسيكون في مؤتمر Hydra 2019 ، الذي سيعقد في 11-12 يوليو 2019 في سانت بطرسبرغ. يمكن شراء التذاكر .
المصدر: www.habr.com