البرمجة القائمة على الثوابت

البرمجة القائمة على الثوابت ^{[ 1 ]} هي منهجية برمجة تُكتب فيها المواصفات والثوابت قبل كتابة عبارات البرنامج الفعلية. لكتابة الثوابت أثناء عملية البرمجة عدة مزايا: فهي تُلزم المبرمج بتوضيح نواياه بشأن سلوك البرنامج قبل تنفيذه فعليًا، كما يمكن تقييم الثوابت ديناميكيًا أثناء التنفيذ لاكتشاف أخطاء البرمجة الشائعة. علاوة على ذلك، إذا كانت الثوابت قوية بما يكفي، فيمكن استخدامها لإثبات صحة البرنامج استنادًا إلى الدلالات الرسمية لعبارات البرنامج. عادةً ما يتطلب التحقق الكامل من البرامج غير البسيطة لغة برمجة ومواصفات مُدمجة، متصلة بنظام إثبات رسمي قوي. في هذه الحالة، يصبح مستوى عالٍ من أتمتة عمليات الإثبات ممكنًا أيضًا.

في معظم لغات البرمجة الحالية، تُعدّ هياكل التحكم في التدفق ، مثل forالحلقات whileوالعبارات ، هي الهياكل التنظيمية الرئيسية. قد لا تكون هذه اللغات مثالية لبرمجة "الثوابت أولاً if" ، لأنها تُجبر المبرمج على اتخاذ قرارات بشأن تدفق التحكم قبل كتابة الثوابت. علاوة على ذلك، لا توفر معظم لغات البرمجة دعمًا جيدًا لكتابة المواصفات والثوابت، نظرًا لافتقارها إلى عوامل التحديد الكمي، وعدم إمكانية التعبير عن خصائص الرتبة العليا فيها عادةً.

نشأت فكرة تطوير البرنامج مع برهانه من إي دبليو ديكسترا . وقد تم النظر في كتابة الثوابت قبل عبارات البرنامج بأشكال مختلفة من قبل إم إتش فان إمدن، وجيه سي رينولدز، وآر جيه باك .

• إيفل (لغة برمجة)