صنف لامتغير

الصنف اللا متغير (أو النوع اللامتغيّر) class invariant (أو type invariant) في برمجة الحاسوب، وعلى وجه التحديد البرمجة الموجهة للكائنات، هو لامتغيّر يستخدم لتقييد كائنات صنف . يجب أن تحافظ طرق الصنف على اللامتغيّر. تقيّد النصف اللامتغيّر الحالة المخزنة في الكائن.

يتم إنشاء لامتغيرات الصنف أثناء البناء ويتم الحفاظ عليها باستمرار بين الاستدغاءات إلى الأساليب العامة. قد يؤدي الكود داخل الدوال إلى كسر اللامتغيرات طالما يتم استعادة اللامتغيرات قبل انتهاء الدالة العامة.

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

جافا

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

public class Date { 
  int /*@spec_public@*/ day;
  int /*@spec_public@*/ hour;

  /*@invariant day >= 1 && day <= 31; @*/ //class invariant
  /*@invariant hour >= 0 && hour <= 23; @*/ //class invariant

  /*@
  @requires d >= 1 && d <= 31;
  @requires h >= 0 && h <= 23;
  @*/
  public Date(int d, int h) { // constructor
    day = d;
    hour = h;
  }

  /*@
  @requires d >= 1 && d <= 31;
  @ensures day == d;
  @*/
  public void setDay(int d) {
    day = d;
  }

  /*@
  @requires h >= 0 && h <= 23;
  @ensures hour == h;
  @*/
  public void setHour(int h) {
    hour = h;
  }
}