دافني

📅 آخر تحديث: ٢٢ يوليو ٢٠٢٦
✍️ نُشر في: ٢٢ يوليو ٢٠٢٦
الموسوعة الحرة

دافني هي لغة برمجة مُجمّعة ، تجمع بين البرمجة الإجرائية والوظيفية ، وتُترجم إلى لغات برمجة أخرى ، مثل C# و Java و JavaScript و Go و Python . تدعم دافني التوصيف الرسمي من خلال الشروط المسبقة واللاحقة ، وثوابت الحلقات ، ومتغيرات الحلقات، ومواصفات الإنهاء ، ومواصفات تأطير القراءة/الكتابة. تجمع اللغة بين أفكار من نموذجي البرمجة الوظيفية والإجرائية ، وتدعم البرمجة كائنية التوجه . تشمل ميزاتها الفئات العامة ، والتخصيص الديناميكي ، وأنواع البيانات الاستقرائية ، ونوعًا من منطق الفصل يُعرف باسم الأطر الديناميكية الضمنية [ 1 ]، وذلك للاستدلال على الآثار الجانبية. [ 2 ] ابتكر دافني روستان لينو في مايكروسوفت للأبحاث، بعد عمله السابق على تطوير ESC/ Modula-3 و ESC/Java وSpec#.

يتم عرض Dafny بانتظام في مسابقات التحقق من البرمجيات (على سبيل المثال VSTTE'08، [ 3 ] VSCOMP'10، [ 4 ] COST'11، [ 5 ] و VerifyThis'12 [ 6 ] ).

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

تعتمد دافني على لغة بوجي الوسيطة التي تستخدم برنامج Z3 الآلي لإثبات النظريات من أجل الوفاء بالتزامات الإثبات. [ 7 ] [ 8 ]

أنواع البيانات

توفر دافني طرقًا للتنفيذ قد يكون لها آثار جانبية، ووظائف تُستخدم في المواصفات وهي وظائف خالصة . [ 9 ] تتكون الطرق من سلاسل من التعليمات البرمجية تتبع أسلوبًا إجرائيًا مألوفًا، بينما يكون جسم الدالة مجرد تعبير. يجب مراعاة أي تعليمات ذات آثار جانبية في الطريقة (مثل إسناد عنصر من مُعامل مصفوفة) من خلال تحديد المعاملات التي يمكن تغييرها باستخدام عبارة `set` modifies. كما توفر دافني مجموعة من أنواع المجموعات غير القابلة للتغيير، بما في ذلك: المتتاليات (مثل `string` )، والمجموعات (مثل `set`)، والخرائط (مثل ` map` )، والصفوف، وأنواع البيانات الاستقرائية، والمصفوفات القابلة للتغيير (مثل `string` ).seq<int>set<int>map<int,int>array<int>

الميزات الأساسية

يوضح ما يلي العديد من الميزات في Dafny، بما في ذلك استخدام الشروط المسبقة والشروط اللاحقة وثوابت الحلقة ومتغيرات الحلقة.

الدالة max(arr:array<int>) تُرجع (max:int) // يجب أن تحتوي المصفوفة على عنصر واحد على الأقل يتطلب أن يكون طول المصفوفة أكبر من صفر // لا يمكن أن تكون القيمة المُعادة أصغر من أي عنصر في المصفوفة يضمن لكل j : int :: j >= 0 && j < arr.Length ==> max >= arr[j] // يجب أن تتطابق القيمة المُعادة مع عنصر ما في المصفوفة يضمن وجود j : int :: j>=0 && j < arr.Length && max == arr[j] { max := arr[0]; var i: int := 1; // بينما (i ​​< طول المصفوفة) // فهرس لا يتجاوز طول المصفوفة (مطلوب لإظهار أن i==arr.Length بعد انتهاء الحلقة) ثابت i <= طول المصفوفة // لم يتم رصد أي عنصر حتى الآن أكبر من الحد الأقصى ثابت لكل j:int :: j >= 0 && j < i ==> max >= arr[j] // بعض العناصر التي تمت رؤيتها حتى الآن تطابق الحد الأقصى يوجد ثابت j:int :: j >= 0 && j < i && max == arr[j] // طول المصفوفة - يتناقص i في كل خطوة ويكون حده الأدنى صفرًا ينقص طول الترتيب - i { // تحديث القيمة القصوى في حال مصادفة عنصر أكبر إذا كان (arr[i] > max) { max := arr[i]; } // استمر في معالجة المصفوفة i := i + 1; } }

يحسب هذا المثال العنصر الأكبر في مصفوفة. يتم تحديد الشرط المسبق والشرط اللاحق للدالة باستخدام عبارات requires`and` ensures(على التوالي). وبالمثل، يتم تحديد ثابت الحلقة ومتغيرها باستخدام عبارات invariant`and` decreases(على التوالي).

ثوابت الحلقة

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

الدالة sumAndZero(arr: array<int>) تُرجع (sum: nat) يتطلب لكل i :: 0 <= i < arr.Length ==> arr[i] >= 0 تعديل المصفوفة { var i: int := 0; المجموع := 0؛ // بينما (i ​​< طول المصفوفة) { المجموع := المجموع + المصفوفة[i]؛ arr[i] := arr[i]; i := i + 1; } }

يفشل هذا التحقق لأن دافني لا تستطيع إثبات صحة (sum + arr[i]) >= 0الشرط عند الإسناد. من الشرط المسبق، من البديهي أن الشرط صحيح داخل الحلقة لأن لا تقوم بأي عملية . مع ذلك، يتسبب هذا الإسناد في تعامل دافني مع كمتغير قابل للتغيير، وبالتالي تجاهل المعلومات المعروفة عنه قبل الحلقة. للتحقق من هذا البرنامج في دافني، يمكننا إما (أ) إزالة الإسناد الزائد ؛ أو (ب) إضافة الشرط الثابت للحلقة.forall i :: 0 <= i < arr.Length ==> arr[i] >= 0arr[i] := arr[i];arrarr[i] := arr[i];invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0

تستخدم دافني أيضًا تحليلًا محدودًا للبرنامج الثابت لاستنتاج ثوابت الحلقات البسيطة حيثما أمكن. في المثال أعلاه، يبدو أن ثابت الحلقة invariant i >= 0مطلوب أيضًا لأن المتغير iيتغير داخل الحلقة. مع أن المنطق الأساسي يتطلب مثل هذا الثابت، إلا أن دافني تستنتجه تلقائيًا، وبالتالي، يمكن حذفه من مستوى الكود المصدري.

ميزات الإثبات

تتضمن دافني ميزات تدعم استخدامها كمساعد في البرهان . على الرغم من أن براهين الخصائص البسيطة داخل عنصر functionأو عنصر آخر method(كما هو موضح أعلاه) ليست غريبة على الأدوات من هذا النوع، إلا أن دافني تسمح أيضًا بإثبات الخصائص بين عنصر functionوآخر. وكما هو شائع في مساعدي البرهان ، غالبًا ما تكون هذه البراهين استقرائية . قد تكون دافني غير معتادة في استخدامها لاستدعاء الدوال كآلية لتطبيق الفرضية الاستقرائية. يوضح المثال التالي ذلك:

datatype List = Nil | Link(data: int, next: List) دالة الجمع (l: قائمة): عدد صحيح { المباراة رقم 1 case Nil => 0 case Link(d, n) => d + sum(n) } predicate isNatList(l: List) { المباراة رقم 1 case Nil => true case Link(d, n) => d >= 0 && isNatList(n) } lemma NatSumLemma(l: List, n: int) يتطلب أن يكون l قائمة طبيعية وأن يكون n مساوياً لمجموع l. يضمن أن يكون n >= 0 { المباراة رقم 1 الحالة Nil => // يتم تفريغها تلقائياً case Link(data, next) => { // تطبيق الفرضية الاستقرائية NatSumLemma(next, sum(next)); // تحقق مما تعرفه دافني تحقق من أن البيانات أكبر من أو تساوي صفرًا؛ } }

هنا، NatSumLemmaتُثبت خاصية مفيدة بينsum() و isNatList()(أي أن isNatList(l) ==> (sum(l) >= 0)). يُعد استخدام ghost methodلترميز الليمات والنظريات أمرًا قياسيًا في دافني، حيث يُستخدم الاستدعاء الذاتي للاستقراء (عادةً، الاستقراء البنيوي ). يتم تحليل الحالاتmatch باستخدام عبارات، وغالبًا ما تُستبعد الحالات غير الاستقرائية تلقائيًا. يجب أن يتمتع المُدقِّق أيضًا بإمكانية الوصول الكامل إلى محتويات functionأو predicateلفكها عند الضرورة. لهذا الأمر آثار عند استخدامه مع مُعدِّلات الوصول . على وجه التحديد، قد يؤدي إخفاء محتويات functionباستخدام protectedالمُعدِّل إلى الحد من الخصائص التي يمكن تحديدها حوله.

انظر أيضاً

مراجع

  1. ↑ سمانس، جان؛ جاكوبس، بارت؛ بيسينز، فرانك (2009). الأطر الديناميكية الضمنية: الجمع بين الأطر الديناميكية ومنطق الفصل (ملف PDF) . وقائع المؤتمر الأوروبي حول البرمجة الكائنية التوجه. الصفحات 148-172 . doi : 10.1007/978-3-642-03013-0_8 . 
  2. ↑ لينو، روستن (2010). دافني: أداة تحقق تلقائية من صحة البرامج الوظيفية . وقائع مؤتمر المنطق للبرمجة والذكاء الاصطناعي والاستدلال. الصفحات 348-370 . doi : 10.1007/978-3-642-17511-4_20 . 
  3. ↑ لينو، روستن؛ موناهان، روزماري (2010). دافني تواجه تحدي معايير التحقق (ملف PDF) . المؤتمر الدولي حول البرمجيات الموثقة: النظريات والأدوات والتجارب. الصفحات 112-116 . doi : 10.1007/978-3-642-15057-9_8 . 
  4. ↑ كليبانوف، فلاديمير؛ وآخرون (2011). مسابقة البرمجيات الموثقة الأولى: تقرير تجريبي . وقائع مؤتمر الأساليب الرسمية. ص 154-168 . CiteSeerX 10.1.1.221.6890 . doi : 10.1007/978-3-642-21437-0_14 .   
  5. ↑ بورمر، ثورستن؛ وآخرون (2011). مسابقة التحقق COST IC0701 لعام 2011. وقائع مؤتمر التحقق الرسمي من البرمجيات الموجهة للكائنات. الصفحات 3-21. CiteSeerX 10.1.1.396.6170 . doi : 10.1007 / 978-3-642-31762-0_2 .   
  6. ↑ هويسمان، ماريكي؛ كليبانوف، فلاديمير؛ موناهان، روزماري (2015). "VerifyThis 2012" (ملف PDF) . المجلة الدولية لأدوات البرمجيات لنقل التكنولوجيا . 17 (6): 647-657 . doi : 10.1007/s10009-015-0396-8 . S2CID 14301377 . 
  7. ↑ "الصفحة الرئيسية لـ Z3" . GitHub . 2019-02-07.
  8. ↑ دي مورا، ليوناردو؛ بيورنر، نيكولاي (2008). Z3: مُحلِّل SMT فعال . وقائع مؤتمر الأدوات والخوارزميات للبناء والتحليل. الصفحات 337-340 . doi : 10.1007/978-3-540-78800-3_24 . 
  9. ↑ "لغة برمجة دافني" . 2022-07-14.

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

  • ماير، برتراند؛ نوردو، مارتن، محرران. (2012). أدوات التحقق العملي من البرمجيات: المدرسة الصيفية الدولية، LASER 2011، جزيرة إلبا، إيطاليا، محاضرات تعليمية منقحة . سبرينغر . ISBN 978-3642357459.
  • سيتنيكوفسكي، بورو (2022). تقديم التحقق من البرمجيات باستخدام لغة دافني: إثبات صحة البرنامج . دار نشر أبريس. رقم ISBN 978-1484279779.