ثابت الحلقة

الموسوعة الحرة

في علوم الحاسوب ، يُعرف ثابت الحلقة بأنه خاصية لحلقة البرنامج تكون صحيحة قبل (وبعد) كل تكرار. وهو عبارة عن تأكيد منطقي ، يُتحقق منه أحيانًا باستخدام تأكيد برمجي . معرفة ثابت (أو ثوابت) الحلقة أمر أساسي لفهم تأثيرها.

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

من منظور منهجية البرمجة، يمكن اعتبار ثابت الحلقة بمثابة مواصفات أكثر تجريدًا للحلقة، تُحدد الغرض الأعمق منها متجاوزةً تفاصيل تنفيذها . تتناول مقالة استعراضية [ 1 ] خوارزميات أساسية من مجالات عديدة في علوم الحاسوب ( البحث ، والفرز ، والتحسين، والحساب، إلخ)، وتُعرّف كلًا منها من منظور ثابتها.

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

مثال غير رسمي

تُعيد الدالة الفرعية التالية في لغة C القيمة القصوى في مصفوفة الوسائط الخاصة بها ، بشرط ألا يقل طولها عن 1. توجد تعليقات في الأسطر 3 و6 و9 و11 و13. يُؤكد كل تعليق على قيم متغير واحد أو أكثر في تلك المرحلة من الدالة. التأكيدات المظللة داخل جسم الحلقة، في بدايتها ونهايتها (السطرين 6 و11)، متطابقة تمامًا. وبالتالي، فهي تصف خاصية ثابتة للحلقة. عند الوصول إلى السطر 13، لا تزال هذه الخاصية الثابتة قائمة، ومن المعروف أن شرط الحلقة من السطر 5 قد أصبح خاطئًا. تشير هاتان الخاصيتان معًا إلى أن القيمة تساوي القيمة القصوى في ، أي أنه يتم إرجاع القيمة الصحيحة من السطر 14.max()a[]ni!=nma[0...n-1]

دالة max ( int ​​n , const int a []) {int m = a [ 0 ];// m تساوي القيمة القصوى في a[0...0]int i = 1 ;بينما ( i ​​!= n ) {// m تساوي القيمة القصوى في a[0...i-1]إذا ( م < أ [ i ])m = a [ i ];// m تساوي القيمة القصوى في a[0...i]++ i ;// m تساوي القيمة القصوى في a[0...i-1]}// m تساوي القيمة القصوى في a[0...i-1]، و i==nأعد m ؛}

باتباع نموذج البرمجة الدفاعيةi!=n ، يُفضّل تعديل شرط الحلقة في السطر 5 إلى i<n، لتجنب التكرار اللانهائي للقيم السالبة غير المسموح بها لـ n. على الرغم من أن هذا التغيير في الكود لا يُفترض أن يُحدث فرقًا، إلا أن المنطق الذي يُبرر صحته يصبح أكثر تعقيدًا، حيث أن قيمة i>=nمعروفة فقط في السطر 13. وللحصول على i<=nالشرط ، يجب تضمين هذا الشرط في ثابت الحلقة. من السهل ملاحظة أن i<=nثابتٌ أيضًا للحلقة، حيث i<nيمكن الحصول على في السطر 6 من شرط الحلقة (المُعدّل) في السطر 5، وبالتالي i<=nيتحقق في السطر 11 بعد iزيادة في السطر 10. مع ذلك، عندما يتعين توفير ثوابت الحلقة يدويًا للتحقق الرسمي من البرنامج، i<=nغالبًا ما يتم تجاهل خصائص بديهية كهذه.

منطق فلويد-هوار

في منطق فلويد-هوار ، [ 2 ] [ 3 ] يتم التحكم في الصحة الجزئية لحلقة while بواسطة قاعدة الاستدلال التالية :

{ج∧أنا}بoدy{أنا}{أنا}wحأنالهـ (ج) بoدy{¬ج∧أنا}{\displaystyle {\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;{\mathtt {while}}\ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}}

هذا يعنى:

  • إذا احتفظ الكود ببعض الخصائص، مثل الخاصية Iبoدy{\displaystyle \mathrm {body} }—وبشكل أدق، إذا استمر الوضع على ما هو عليه بعد تنفيذبoدy{\displaystyle \mathrm {body} }عندما كان كل من C و I متمسكين مسبقًا - ( السطر العلوي)
  • يُضمن أن تكون C و I خاطئة وصحيحة، على التوالي، بعد تنفيذ الحلقة بأكملهاwحأنالهـ (ج) بoدy{\displaystyle {\mathtt {while}}\ (C)\ \mathrm {body} }، بشرط أن تكون القيمة صحيحة قبل الحلقة (السطر السفلي) .

بمعنى آخر: القاعدة المذكورة أعلاه هي خطوة استنتاجية تنطلق من ثلاثية هوار.{ج∧أنا}بoدy{أنا}{\displaystyle \{C\land I\}\;\mathrm {body} \;\{I\}}هذه الثلاثية هي في الواقع علاقة بين حالات الآلة. وهي صحيحة عند البدء من حالة يكون فيها التعبير المنطقيج∧أنا{\displaystyle C\land I}صحيح، ويتم تنفيذ بعض التعليمات البرمجية بنجاح.بoدy{\displaystyle \mathrm {body} }، ينتهي المطاف بالآلة في حالة تكون فيها I صحيحة. إذا أمكن إثبات هذه العلاقة، فإن القاعدة تسمح لنا بالاستنتاج بأن التنفيذ الناجح للبرنامجwحأنالهـ (ج) بoدy{\displaystyle {\mathtt {while}}\ (C)\ \mathrm {body} }سيؤدي ذلك من حالة يكون فيها "أنا " صادقًا إلى حالة يكون فيها¬ج∧أنا{\displaystyle \lnot C\land I}صحيح. تُسمى الصيغة المنطقية I في هذه القاعدة ثابت الحلقة.

مع بعض الاختلافات في الترميز المستخدم، وبافتراض توقف الحلقة، تُعرف هذه القاعدة أيضًا باسم نظرية العلاقة الثابتة . [ 4 ] [ 5 ] كما يقدمها أحد الكتب الدراسية في سبعينيات القرن الماضي بطريقة تهدف إلى أن تكون في متناول طلاب البرمجة: [ 4 ]

لنفترض أن الرمز P { seq } Qيعني أنه إذا Pكانت العبارة صحيحة قبل تنفيذ سلسلة العبارات seq، فإنها Qتكون صحيحة بعدها. عندئذٍ، تنطبق نظرية العلاقة الثابتة.

P & c { seq } P
يشير إلى
P { DO WHILE (c); seq END; } P & ¬c

مثال

يوضح المثال التالي كيفية عمل هذه القاعدة. لنفترض البرنامج التالي:

بينما (س < ١٠) x := x+1;

يمكن للمرء بعد ذلك إثبات ثلاثية هوار التالية:

{x≤10}wحأنالهـ (x<10) x:=x+1{x=10}{\displaystyle \{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{x=10\}}

الشرط C للحلقة whileهوx<10{\displaystyle x<10}يجب تخمين الثابت المفيد للحلقة I ؛ وسيتضح لاحقًا أنx≤10{\displaystyle x\leq 10}هذا مناسب. في ظل هذه الافتراضات، يمكن إثبات ثلاثية هوار التالية:

{x<10∧x≤10}x:=x+1{x≤10}{\displaystyle \{x<10\land x\leq 10\}\;x:=x+1\;\{x\leq 10\}}

على الرغم من إمكانية اشتقاق هذه الثلاثية رسميًا من قواعد منطق فلويد-هوار التي تحكم التخصيص، إلا أنها مبررة بديهيًا أيضًا: تبدأ العملية الحسابية في حالة حيثx<10∧x≤10{\displaystyle x<10\land x\leq 10}هذا صحيح، وهذا يعني ببساطة أنx<10{\displaystyle x<10}هذا صحيح. تضيف العملية الحسابية 1 إلى x ، مما يعني أنx≤10{\displaystyle x\leq 10}لا يزال هذا صحيحًا (بالنسبة للعدد الصحيح x).

وبناءً على هذه الفرضية، تسمح قاعدة whileالحلقات بالاستنتاج التالي:

{x≤10}wحأنالهـ (x<10) x:=x+1{¬(x<10)∧x≤10}{\displaystyle \{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{\lnot (x<10)\land x\leq 10\}}

ومع ذلك، فإن الشرط اللاحق¬(x<10)∧x≤10{\displaystyle \lnot (x<10)\land x\leq 10}( x أقل من أو يساوي 10، ولكنه ليس أقل من 10) مكافئ منطقياً لـx=10{\displaystyle x=10}وهذا ما أردنا إظهاره.

العقار0≤x{\displaystyle 0\leq x}وهي خاصية ثابتة أخرى لحلقة المثال، والخاصية التافهةترuهـ{\displaystyle \mathrm {true} }وهناك مثال آخر. بتطبيق قاعدة الاستدلال المذكورة أعلاه على الثابت السابق، نحصل على{0≤x}wحأنالهـ (x<10) x:=x+1{10≤x}{\displaystyle \{0\leq x\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}}تطبيق ذلك على الثابتترuهـ{\displaystyle \mathrm {true} }العائد{ترuهـ}wحأنالهـ (x<10) x:=x+1{10≤x}{\displaystyle \{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}}وهو أكثر تعبيراً قليلاً.

دعم لغات البرمجة

إيفل

توفر لغة البرمجة إيفل دعمًا أصليًا لثوابت الحلقات . [ 6 ] يُعبَّر عن ثابت الحلقة بنفس الصيغة المستخدمة لثابت الفئة . في المثال أدناه، يجب أن يكون تعبير ثابت الحلقة صحيحًا بعد تهيئة الحلقة، وبعد كل تنفيذ لجسم الحلقة؛ ويتم التحقق من ذلك أثناء التشغيل.x <= 10

من x := 0 ثابت x <= 10 حتى x > 10 حلقة x := x + 1 نهاية

وايلي

توفر لغة البرمجة Whiley أيضًا دعمًا ممتازًا لثوابت الحلقات. [ 7 ] تُعبَّر ثوابت الحلقات باستخدام whereبند واحد أو أكثر، كما هو موضح أدناه:

دالة max ( int [] items ) -> ( int r ) // تتطلب عنصرًا واحدًا على الأقل لحساب القيمة القصوى، أي أن | items | > 0 // (1) النتيجة ليست أصغر من أي عنصر، مما يضمن أن جميع { i في 0 .. | items | | items [ i ] <= r } // (2) النتيجة تطابق عنصرًا واحدًا على الأقل ، مما يضمن أن بعض { i في 0 .. | items | | items [ i ] == r } : // عدد طبيعي i = 1 int m = items [ 0 ] // بينما i < | items | // (1) لا يوجد عنصر تمت رؤيته حتى الآن أكبر من m حيث جميع { k في 0 .. i | items [ k ] <= m } // (2) عنصر واحد أو أكثر تمت رؤيته حتى الآن يطابق m حيث بعض { k في 0 .. i | items [ k ] == m } : إذا كان items [ i ] > m : m = items [ i ] i = i + 1 // إرجاع m

تحدد هذه max()الدالة أكبر عنصر في مصفوفة أعداد صحيحة. ولكي يتم تحديدها، يجب أن تحتوي المصفوفة على عنصر واحد على الأقل. تتطلب الشروط اللاحقة أن max()تكون القيمة المُعادة: (1) ليست أصغر من أي عنصر؛ و(2) أنها تُطابق عنصرًا واحدًا على الأقل. يتم تعريف ثابت الحلقة استقرائيًا من خلال بندين where، كل منهما يُقابل بندًا في الشرط اللاحق. الفرق الأساسي هو أن كل بند من بنود ثابت الحلقة يُحدد أن النتيجة صحيحة حتى العنصر الحالي i، بينما تُحدد الشروط اللاحقة أن النتيجة صحيحة لجميع العناصر.

استخدام ثوابت الحلقة

يمكن أن يخدم ثابت الحلقة أحد الأغراض التالية:

  1. وثائقي بحت
  2. يتم التحقق من ذلك داخل الكود، على سبيل المثال، عن طريق استدعاء تأكيد.
  3. سيتم التحقق من ذلك بناءً على منهج فلويد-هوار

بالنسبة للنقطة الأولى، يكفي التعليق باللغة الطبيعية (كما // m equals the maximum value in a[0...i-1]في المثال أعلاه ).

بالنسبة للنقطة الثانية، يلزم دعم لغة برمجة، مثل مكتبة assert.h في لغة C ، أو العبارة الموضحة أعلاه في لغة Eiffel. غالبًا ما يمكن تفعيل أو تعطيل التحقق أثناء التشغيل (لأغراض تصحيح الأخطاء) بواسطة المُصرّف أو خيار وقت التشغيل.invariant

بالنسبة للنقطة 3، توجد بعض الأدوات لدعم البراهين الرياضية، والتي عادة ما تستند إلى قاعدة فلويد-هوار الموضحة أعلاه ، والتي تنص على أن رمز الحلقة المعطى يفي في الواقع بـ (مجموعة من) ثوابت الحلقة المعطاة.

يمكن استخدام تقنية التفسير المجرد للكشف التلقائي عن ثوابت الحلقات في الكود المعطى. ومع ذلك، يقتصر هذا النهج على الثوابت البسيطة جدًا (مثل 0<=i && i<=n && i%2==0...).

التمييز عن الكود غير المتغير في الحلقة

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

for ( int i = 0 ; i < n ; ++ i ) { x = y + z ; a [ i ] = 6 * i + x * x ; }

حيث يمكن نقل العمليات الحسابية x = y+zقبل x*xالحلقة، مما ينتج عنه برنامج مكافئ، ولكنه أسرع:

x = y + z ; t1 = x * x ; for ( int i = 0 ; i < n ; ++ i ) { a [ i ] = 6 * i + t1 ; }

على النقيض من ذلك، على سبيل المثال، الخاصية 0<=i && i<=nهي ثابت الحلقة لكل من البرنامج الأصلي والبرنامج المحسن، ولكنها ليست جزءًا من الكود، وبالتالي لا معنى للحديث عن "إخراجها من الحلقة".

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

x1 = y + z ; t1 = x1 * x1 ; for ( int i = 0 ; i < n ; ++ i ) { x2 = y + z ; a [ i ] = 6 * i + t1 ; }

إحدى الخصائص الثابتة لهذا الكود هي (x1==x2 && t1==x2*x2) || i==0، مما يشير إلى أن القيم المحسوبة قبل الحلقة تتفق مع تلك المحسوبة داخلها (باستثناء ما قبل التكرار الأول).

انظر أيضاً

مراجع

  1. ↑ فوريا، كارلو أ.؛ ماير، برتراند؛ فيلدر، سيرجي (13 يناير 2014)، "ثوابت الحلقات: التحليل والتصنيف والأمثلة"، مجلة ACM Computing Surveys ، 46 (3): 1-51 ، arXiv : 1211.4470 ، doi : 10.1145/2506375
  2. ↑ روبرت و. فلويد (1967). "إسناد معانٍ للبرامج" (ملف PDF) . في جيه تي شوارتز (محرر). وقائع الندوات في الرياضيات التطبيقية . الجوانب الرياضية لعلوم الحاسوب. المجلد 19. بروفيدنس، رود آيلاند: الجمعية الرياضية الأمريكية. الصفحات 19-32 .  
  3. ↑ هوار، سي. أ. ر. (أكتوبر 1969). "أساس بديهي لبرمجة الحاسوب" . اتصالات رابطة آلات الحوسبة . 12 (10): 576-580 . doi : 10.1145/363235.363259 . S2CID 207726175 . 
  4. 1 2 كونواي، ريتشارد ؛ غريس، ديفيد (1973). مقدمة في البرمجة: منهج منظم باستخدام PL/1 وPL/C . كامبريدج، ماساتشوستس: وينثروب. ص 198-200 . 
  5. ↑ هوانغ، جيه سي (2009). اكتشاف أخطاء البرمجيات من خلال الاختبار والتحليل . هوبوكين، نيو جيرسي: جون وايلي وأولاده. ص 156-157 . 
  6. ↑ ماير، برتراند ، إيفل: اللغة، برنتيس هول ، 1991، ص 129-131.
  7. ↑ بيرس، ديفيد جيه؛ غروفز، ليندسي (2015). "تصميم مُصرّف مُدقّق: دروس مُستفادة من تطوير وايلي". علم برمجة الحاسوب . 113 : 191-220 . doi : 10.1016/j.scico.2015.09.006 .

للمزيد من القراءة