Whiel می‌کوشد صحت برنامه‌های رابطه‌ای را با گواهی Lean بررسی کند

پژوهشگران در پیش‌چاپی در arXiv سامانهٔ Whiel را معرفی کرده‌اند؛ ابزاری برای استدلالِ گواهی‌شده با Lean دربارهٔ برنامه‌های رابطه‌ایِ امری. این سامانه می‌تواند مسئله‌های شمول و هم‌ارزی در Datalog، گونه‌های دارای نفی و بخش اصلی زبان‌های پرس‌وجوی گرافی را کدگذاری کند.

Whiel همچنین قادر است الگوریتم‌های بهینه‌سازی‌شده یا افزایشی برای ارزیابی پرس‌وجوها را نمایش دهد؛ الگوریتم‌هایی که لزوماً در زبان پرس‌وجوی اولیه قابل بیان نیستند. مشخصات مرتبه‌اولِ محدودیت‌های یکپارچگی، نگاشت طرح‌واره‌ها و نماها در یکپارچه‌سازی، تبادل و اشتراک داده نیز در دامنهٔ آن قرار می‌گیرند.

در این سامانه، وضعیت برنامه با یک نمونهٔ پایگاه داده نمایش داده می‌شود و ساختار امری برنامه امکان استدلال ترکیبی به سبک Hoare را با مشخصات رابطه‌ای مرتبه‌اول فراهم می‌کند. Whiel برای پشتیبانی از استدلال‌های استقرایی از متغیرهای پیش‌گویی و ناورداهای چندسطحی بهره می‌گیرد. سامانه به‌صورت عصبی‌نمادین ناورداهای حلقه را پیشنهاد می‌دهد؛ شرط‌های لازم برای بررسی آن‌ها را برهان‌گر مرتبه‌اول Vampire می‌سنجد و راه‌حل‌های پیشنهادی در قالب گواهی‌های اثبات Lean ترجمه می‌شوند. ضد‌مثال‌ها نیز به فرایند عصبی‌نمادین بازگردانده می‌شوند.

پژوهشگران عملکرد Whiel را روی مجموعه‌ای گزینش‌شده از آزمون‌ها ارزیابی کرده‌اند، اما چکیده جزئیات نتایج را گزارش نمی‌کند. آنان این سامانه را ابزاری بالقوه برای مسائل دشوار و معمولاً تصمیم‌ناپذیر در زبان‌های پیچیدهٔ پرس‌وجو و محدودیت می‌دانند و بر اعتمادپذیری خروجی آن تأکید می‌کنند.