صنف لامتغير
قبل الخوض في التفاصيل، الصنف اللا متغير (أو النوع اللامتغيّر) class invariant (أو type invariant) في برمجة الحاسوب، وعلى وجه التحديد البرمجة الموجهة للكائنات، هو لامتغيّر يستعمل لتقييد كائنات صنف . يجب أن تحافظ طرق الصنف على اللامتغيّر. تقيّد النصف اللامتغيّر الحالة المخزنة في الكائن. وتعرض الأقسام التالية جوانب أخرى من الموضوع.
ومن جهة أخرى، الكائن اللامتغّير، أو التمثيل اللامتغيّر، هو بنية برمجة حاسوبية تتكون من مجموعة من الخصائص اللامتغيّرة التي لا تتنازل بغض النظر عن حالة الكائن. هذا يضمن أن الكائن سيلبي دائمًا الشروط المحددة مسبقًا، وبالتالي فإن الطرق قد تشير دائمًا إلى الكائن دون المخاطرة بالافتراضات غير الدقيقة. يمكن أن يساعد تعريف اللامتغيرات الصنفية المبرمجين والمختبرين على التقاط المزيد من الأخطاء أثناء اختبار البرمجيات.
ومن ناحية أخرى، يتم إنشاء لامتغيرات الصنف أثناء البناء ويتم الحفاظ عليها باستمرار بين الاستدغاءات إلى الأساليب العامة. قد يؤدي الكود داخل الدوال إلى كسر اللامتغيرات طالما يتم استعادة اللامتغيرات قبل انتهاء الدالة العامة.
/*@
- @requires d >= 1 && d <= 31;
- @ensures day == d;
- @*/
- public void setDay(int d) {
- day = d;
- }
جافا
وفي هذا السياق، هذا مثال لصنف لا متغيّر في لغة برمجة جافا باستخدام لغة لغة نمذجة جافا . يجب أن يحافظ اللامتغيّر على قيمة صحيح ture بعد الانتهاء من المنشئ وعند الدخول والخروج من جميع الطرق العامة. يجب أن تحدد الطرق العامة الشرط المسبق والشرط اللاحق للمساعدة في ضمان لاتغيّر الصنف.public class Date {
int /*@spec_public@*/ day;
/*@
@requires d >= 1 && d <= 31;
@requires h >= 0 && h <= 23;
/*@
- @requires h >= 0 && h <= 23;
- @ensures hour == h;
- @*/
- public void setHour(int h) {
- hour = h;
- }
- }
@*/
- public Date(int d, int h) { // constructor
- day = d;
- hour = h;
- }
int /*@spec_public@*/ hour;
/*@invariant hour >= 0 && hour <= 23; @*/ //class invariant
/*@invariant day >= 1 && day <= 31; @*/ //class invariant
📝 هل في هذه المقالة خطأ؟
إذا وجدت معلومة تحتاج تصحيحاً أو إضافة، أو أردت حذف المقالة، أرسل لنا طلباً وسنراجعه.
ما رأيك في هذه المقالة؟