وايلي (لغة برمجة)

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

بدأ مشروع Whiley في عام 2009 استجابةً لتحدي "التحقق من صحة المترجم" الذي طرحه توني هوار في عام 2003. ^{[ 2 ]} وكان أول إصدار عام من Whiley في يونيو 2010. ^{[ 3 ]}

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

يقوم مترجم Whiley بإنشاء التعليمات البرمجية لآلة جافا الافتراضية (JVM) ويمكنه التفاعل مع جافا واللغات الأخرى القائمة على JVM.

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

يستخدم المترجم المدقق الاستدلال الرياضي والمنطقي للتحقق من صحة البرامج التي يقوم بتجميعها.

يتمثل الهدف الرئيسي من هذه الأداة في تحسين جودة البرمجيات من خلال ضمان استيفاء البرنامج لمواصفات رسمية . ويأتي هذا في أعقاب العديد من المحاولات لتطوير أدوات مماثلة، بما في ذلك جهود بارزة مثل SPARK/Ada و ESC/Java وSpec# و Dafny وWhy3 ^{[ 7 ]} و Frama-C .

ركزت معظم المحاولات السابقة لتطوير مُصرّف مُدقّق على توسيع لغات البرمجة الحالية بإضافة بنيات لكتابة المواصفات. على سبيل المثال، تُضيف لغة ESC/Java ولغة نمذجة جافا (Java Modeling Language) تعليقات توضيحية لتحديد الشروط المسبقة واللاحقة في جافا . وبالمثل، تُضيف Spec# و Frama-C بنيات مماثلة إلى لغتي C# و C. مع ذلك، تحتوي هذه اللغات على العديد من الميزات التي تُشكّل تحديات صعبة أو مستعصية أمام عملية التحقق. ^{[ 8 ]} في المقابل، صُممت لغة Whiley من الصفر في محاولة لتجنب الأخطاء الشائعة وجعل عملية التحقق أكثر سهولة. ^{[ 9 ]}

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

يميز Whiley بين نوع البيانات `a` function(وهو نوع بيانات نقي ) ونوع البيانات `a` method(الذي قد يكون له آثار جانبية ). هذا التمييز ضروري لأنه يسمح باستخدام الدوال في المواصفات. تتوفر مجموعة مألوفة من أنواع البيانات الأولية bool، بما في ذلك ` inta` و`b` و`arrays` (مثل `a` و` int[]b`) و`records` (مثل `a` و`records` {int x, int y}). مع ذلك، وخلافًا لمعظم لغات البرمجة، فإن نوع البيانات ` inta` غير محدود ولا يتوافق مع تمثيل ذي عرض ثابت مثل المتمم الثنائي 32 بت . بالتالي، يمكن للعدد الصحيح غير المقيد في Whiley أن يأخذ أي قيمة عددية صحيحة ممكنة، مع مراعاة قيود الذاكرة لبيئة التشغيل. يُبسط هذا الخيار عملية التحقق، لأن التفكير المنطقي في الحساب النمطي مشكلة معروفة ومعقدة. الكائنات المركبة (مثل المصفوفات أو السجلات) ليست مراجع لقيم في الذاكرة الديناميكية كما هو الحال في لغات مثل Java أو C#، بل هي قيم غير قابلة للتغيير .

تتبع لغة Whiley نهجًا غير مألوف في التحقق من الأنواع يُسمى " التحقق من الأنواع المتدفقة" . يمكن أن يكون للمتغيرات أنواع ثابتة مختلفة في نقاط مختلفة من الدالة أو الأسلوب. يشبه التحقق من الأنواع المتدفقة التحقق من الأنواع عند حدوثها كما هو موجود في Typed Racket . ^{[ 10 ]} ولتسهيل التحقق من الأنواع المتدفقة، تدعم Whiley أنواع الاتحاد والتقاطع والنفي. ^{[ 11 ]} تُقارن أنواع الاتحاد بأنواع الجمع الموجودة في اللغات الوظيفية مثل Haskell ، ولكنها في Whiley ليست منفصلة. تُستخدم أنواع التقاطع والنفي في سياق التحقق من الأنواع المتدفقة لتحديد نوع المتغير على فرعي "صحيح" و"خطأ" لاختبار نوع وقت التشغيل. على سبيل المثال، لنفترض أن لدينا متغيرًا xمن النوع `a` Tواختبار نوع وقت التشغيل ` x is Sb`. على الفرع "صحيح"، xيصبح نوع `a` هو `b` T & S، بينما على الفرع "خطأ"، يصبح `b` هو `b` T & !S.

تستخدم لغة وايلي نظام أنواع هيكلي بدلاً من نظام الأنواع الاسمي . وتُعدّ لغات مودولا-3 وجو وسيلون أمثلة على لغات أخرى تدعم الكتابة الهيكلية بشكل أو بآخر.

يدعم Whiley دورات حياة مرجعية مشابهة لتلك الموجودة في Rust . يمكن تحديد دورات الحياة عند تخصيص كائنات جديدة للإشارة إلى الوقت المناسب لتحريرها بأمان. يجب أن تتضمن المراجع إلى هذه الكائنات مُعرّف دورة الحياة لمنع المراجع المعلقة . لكل دالة دورة حياة ضمنية يُشار إليها بـ `. يُمثل متغير من النوع `< ...`<``<```<` this` ` `&this:TT&l1:T&l2:Tl1l2

لا يحتوي Whiley على دعم مدمج للتزامن ولا يوجد نموذج ذاكرة رسمي لتحديد كيفية تفسير القراءة / الكتابة إلى حالة قابلة للتغيير مشتركة.

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

// تعريف نوع الأعداد الطبيعية type nat is ( int x ) where x >= 0public function indexOf ( int [] items , int item ) -> ( int | null index ) // إذا تم إرجاع int، فإن العنصر في هذا الموضع يطابق item، مما يضمن أن يكون الفهرس int ==> items [ index ] == item // إذا تم إرجاع int، فإن العنصر في هذا الموضع هو أول تطابق، مما يضمن أن يكون الفهرس int ==> no { i in 0 .. index | items [ i ] == item } // إذا تم إرجاع null، فلا يوجد عنصر في items يطابق item، مما يضمن أن يكون الفهرس null ==> no { i in 0 .. | items | | items [ i ] == item } : // nat i = 0 // while i < | items | // لم يتم رؤية أي عنصر حتى الآن يطابق item حيث no { j in 0 .. i | items [ j ] == item } : // if items [ i ] == item : return i i = i + 1 // return null

في المثال أعلاه، تم تحديد نوع الإرجاع للدالة كنوع اتحاد، int|nullمما يشير إلى إمكانية إرجاع قيمة ما . يتكون شرط ما بعد التنفيذ للدالة من ثلاثة بنود، يصف كل منها خصائص مختلفة يجب أن تتحقق في القيمة المُعادة . يُستخدم تحديد نوع التدفق في هذه البنود من خلال عامل اختبار نوع وقت التشغيل . على سبيل المثال، في البند الأول ، يُعاد تحديد نوع المتغير من إلى مباشرةً على الجانب الأيمن من عامل الاستلزام (أي ).intnullensuresindexisensuresindexint|nullint==>

يوضح المثال أعلاه أيضًا استخدام ثابت الحلقة الاستقرائي . يجب إثبات صحة ثابت الحلقة عند الدخول إلى الحلقة، وفي أي تكرار مُعطى لها، وعند الخروج منها. في هذه الحالة، يُحدد ثابت الحلقة ما هو معروف عن عناصر المصفوفة التي itemsتم فحصها حتى الآن، أي أن أيًا منها لا يُطابق المصفوفة المُعطاة item. لا يؤثر ثابت الحلقة على معنى البرنامج، ويمكن اعتباره غير ضروري إلى حد ما. مع ذلك، يُعد ثابت الحلقة ضروريًا لمساعدة المُدقِّق الآلي المُستخدم في مُصرِّف Whiley على إثبات أن هذه الدالة تُطابق مواصفاتها.

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

بدأ تطوير لغة وايلي في عام ٢٠٠٩ مع أول إصدار علني، v0.2.27تلاه إصداران آخران في يونيو ٢٠١٠ v0.3.0وسبتمبر من العام نفسه. وقد تطورت اللغة ببطء مع العديد من التغييرات في بناء الجملة حتى الآن. دعمت الإصدارات السابقة أنواع البيانات v0.3.33من الدرجة الأولى ، ولكن تم حذفها لصالح تمثيل السلاسل النصية كمصفوفات مقيدة. وبالمثل، دعمت الإصدارات السابقة مجموعات من الدرجة الأولى (مثل `set` )، وقواميس (مثل `dictionary`)، وقوائم قابلة لتغيير الحجم (مثل `resume` )، ولكن تم التخلي عنها لصالح المصفوفات البسيطة (مثل `array` ). ولعلّ أكثر ما أثار الجدل هو حذف نوع البيانات `set` في الإصدار `resume` . وقد كان الدافع وراء العديد من هذه التغييرات هو الرغبة في تبسيط اللغة وتسهيل تطوير المترجم.stringcharint[]v0.3.35{int}{int=>bool}[int]int[]realv0.3.38

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

• الموقع الرسمي
• ويلي على جيت هاب