ثابت الفئة

تدعم لغة البرمجة Ada بشكلٍ أصيل ثوابت النوع (بالإضافة إلى الشروط المسبقة واللاحقة، ومسندات الأنواع الفرعية، وما إلى ذلك). يمكن تحديد ثابت النوع على نوع خاص (على سبيل المثال، لتحديد علاقة بين خصائصه المجردة)، أو على تعريفه الكامل (عادةً للمساعدة في التحقق من صحة تنفيذ النوع). ^{[ 6 ]} فيما يلي مثال على ثابت نوع مُحدد على التعريف الكامل لنوع خاص يُستخدم لتمثيل مكدس منطقي. يستخدم التنفيذ مصفوفة، ويحدد ثابت النوع خصائص معينة للتنفيذ تُمكّن من إثبات السلامة. في هذه الحالة، يضمن الثابت أنه بالنسبة لمكدس ذي عمق منطقي N، فإن أول N عنصر من المصفوفة هي قيم صالحة. يضمن الشرط الابتدائي الافتراضي لنوع Stack، من خلال تحديد مكدس فارغ، صحة الثابت في البداية، ويحافظ Push على الثابت. تُمكّن صحة الشرط الثابت دالة Pop من الاعتماد على حقيقة أن أعلى المكدس قيمة صالحة، وهو ما يلزم لإثبات شرط ما بعد التنفيذ لدالة Pop. يُمكّن شرط ثابت أكثر تعقيدًا من إثبات صحة الوظيفة بالكامل، مثل أن دالة Pop تُعيد القيمة المُمرّرة إلى دالة Push المقابلة، ولكن في هذه الحالة نحاول فقط إثبات أن دالة Pop لا تُعيد قيمة غير صالحة (Invalid_Value).

النوع العام Item خاص ؛ Invalid_Value : في Item ؛ الحزمة Stacks هي نوع Stack ( العمق الأقصى : موجب ) خاص مع Default_Initial_Condition = > Is_Empty ( Stack ) ؛دالة Is_Empty ( S : في Stack ) تُرجع قيمة منطقية ؛ دالة Is_Full ( S : في Stack ) تُرجع قيمة منطقية .إجراء Push ( S : إدخال/ إخراج Stack ؛ I : إدخال Item ) مع Pre => not Is_Full ( S ) ثم I /= Invalid_Value ، Post => not Is_Empty ( S )؛ إجراء Pop ( S : إدخال/إخراج Stack ؛ I : إخراج Item ) مع Pre = > not Is_Empty ( S )، Post => not Is_Full ( S ) ثم I /= Invalid_Value ؛ نوع Item_Array خاص هو مصفوفة ( نطاق موجب <>) من Item ؛نوع Stack ( العمق الأقصى : موجب ) هو سجل طوله : طبيعي := 0 ؛ بياناته : مصفوفة عناصر ( 1 .. العمق الأقصى ) := ( الآخرون => قيمة غير صالحة )؛ نهاية السجل مع نوع ثابت => الطول <= العمق الأقصى، ثم ( لكل J في 1 .. الطول = > بيانات ( J ) / = قيمة غير صالحة )؛دالة Is_Empty ( S : في Stack ) تُرجع قيمة منطقية is ( S.Length = 0 ) ؛ دالة Is_Full ( S : في Stack ) تُرجع قيمة منطقية is ( S.Length = S.Max_Depth ) ؛ نهاية Stacks ؛​​

تدعم لغة البرمجة D بشكلٍ أصلي ثوابت الفئات، بالإضافة إلى تقنيات البرمجة التعاقدية الأخرى . إليك مثال من الوثائق الرسمية. ^{[ 7 ]}

class Date { int day ; int hour ;invariant () { assert ( day >= 1 && day <= 31 ); assert ( hour >= 0 && hour <= 23 ); } }

في لغة إيفل ، يظهر الثابت الخاص بالفئة في نهاية الفئة بعد الكلمة المفتاحية invariant.

تاريخ الحصةاصنع​الميزة { لا شيء } -- التهيئةإنشاء ( a_day : عدد صحيح ; a_hour : عدد صحيح ) -- تهيئة `Current` باستخدام `a_day` و`a_hour`. يتطلب valid_day : a_day >= 1 و a_day <= 31 valid_hour : a_hour >= 0 و a_hour <= 23 do day := a_day hour := a_hour ensure day_set : day = a_day hour_set : hour = a_hour endميزة -- الوصولاليوم : عدد صحيح -- يوم الشهر لـ "الحالي"الساعة : عدد صحيح -- ساعة اليوم لـ "الحالي"ميزة -- تغيير العنصرset_day ( a_day : INTEGER ) -- تعيين قيمة `day` إلى `a_day` يتطلب valid_argument : a_day >= 1 و a_day <= 31 do day := a_day ensure day_set : day = a_day endset_hour ( a_hour : INTEGER ) -- تعيين قيمة `hour` إلى `a_hour` يتطلب valid_argument : a_hour >= 0 و a_hour <= 23 do hour := a_hour ensure hour_set : hour = a_hour endثابت valid_day : اليوم >= 1 واليوم <= 31 ، ثابت valid_hour : الساعة >= 0 والساعة <= 23 نهاية

توفر مكتبة Loki (C++) إطار عمل كتبه ريتشارد سبوساتو للتحقق من ثوابت الفئة، وثوابت البيانات الثابتة، ومستوى أمان الاستثناءات .

هذا مثالٌ على كيفية استخدام فئةٍ ما لـ Loki::Checker للتحقق من بقاء الثوابت صحيحةً بعد تغيير كائنٍ ما. يستخدم المثال كائن نقطة جغرافية لتخزين موقعٍ على سطح الأرض كإحداثياتٍ لخط العرض وخط الطول.

الثوابت الجغرافية هي:

• لا يجوز أن يتجاوز خط العرض 90 درجة شمالاً.
• لا يجوز أن يقل خط العرض عن -90 درجة جنوباً.
• لا يجوز أن يتجاوز خط الطول 180 درجة شرقاً.
• لا يجوز أن يكون خط الطول أقل من -180 درجة غرباً.

استيراد <cassert> ؛ استيراد < loki / Checker.h > ؛​​​​تصدير الوحدة النمطية ويكيبيديا . أمثلة . نقطة جغرافية ؛استيراد wikipedia.examples.Degrees ؛​​​​باستخدام ويكيبيديا :: أمثلة :: درجات ؛/** * مطلوب للتحقق من ثوابت الفئة. * @note تقوم الدالة CheckFor بفحص صحة العديد من الدوال لتحديد * ما إذا كان الكود قد انتهك أيًا من الثوابت، أو ما إذا كان أي محتوى قد تغير، أو ما إذا * أطلقت الدالة استثناءً. */ using Loki :: CheckFor ;namespace wikipedia :: examples {export class GeoPoint { private : /// تتحقق هذه الدالة من جميع ثوابت الكائن. bool isValid () const { assert ( this ); assert ( latitude >= -90.0 ); assert ( latitude <= 90.0 ); assert ( longitude >= -180.0 ); assert ( longitude <= 180.0 ); return true ; }درجات خط العرض ؛ ///< الدرجات من خط الاستواء. الموجب شمالاً، والسالب جنوباً. درجات خط الطول ؛ ///< الدرجات من خط غرينتش. الموجب شرقاً، والسالب غرباً. عام : نقطة جغرافية ( درجات خط العرض ، درجات خط الطول )؛/// تقوم دالة Move بنقل موقع GeoPoint. void move ( Degrees latChange , Degrees lonChange ) { // يستدعي كائن التحقق IsValid عند دخول الدالة وخروجها للتحقق من صحة كائن GeoPoint هذا. يضمن المدقق أيضًا أن دالة GeoPoint::move لن تُطلق أي استثناء. CheckFor < const GeoPoint >:: CheckForNoThrow checker ( this , & isValid );latitude += latChange ; if ( latitude >= 90.0f ) { latitude = 90.0f ; } if ( latitude <= -90.0f ) { latitude = -90.0f ; }longitude += lonChange ; while ( longitude >= 180.0f ) { longitude -= 360.0f ; } while ( longitude <= -180.0f ) { longitude += 360.0f ; } } };}

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

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 ; } }