بیا یه کم درباره یکی از قابلیت‌های جدید و باحال توی ابزار ACL2 حرف بزنیم. اگه تا حالا اسم ACL2 به گوشت نخورده، بدون که یه ابزار قدرتمنده که بیشتر توی چک‌کردن و اثبات برنامه‌ها کاربرد داره؛ مخصوصا برنامه‌هایی که حساس هستن و نباید خطا داشته باشن.
حالا تازه‌ترین نسخه ACL2 که در اکتبر ۲۰۲۴ معرفی شد (ورژن 8.6)، یه قابلیت جالب اضافه کرده به اسم attach-stobj. خب، این attach-stobj چیه؟
بذار ساده بگم: گاهی تو برنامه‌نویسی یه چیزی به اسم “stobj” داریم. stobj یعنی “State Object”، یه نوع خاص از شیء که حالت یا وضعیت برنامه رو تو خودش نگه می‌داره و جوری طراحی شده که اجرا سریع‌تر بشه. حالا مشکل اینه که بعضی وقتا می‌خوای برای این stobj چند جور رفتار یا پیاده‌سازی مختلف داشته باشی. مثلاً شاید بخوای نسخه‌ای ازش باشه که سریع اما ساده است، یا یکی دیگه که تست‌محوره و خروجی رو بررسی می‌کنه.
قبلا اگه می‌خواستی این کار رو بکنی باید برمی‌گشتی و کلی کد و اثبات دوباره انجام می‌دادی، واسه همین کار یکم کابوس بود! اما با این قابلیت attach-stobj، می‌تونی چندین جور پیاده‌سازی اجراشوندنی (یا به اصطلاح operations) رو به یک stobj ربط بدی، بدون اینکه لازم باشه دوباره نگران کلی بازبینی و تأیید و این‌جور داستان‌ها باشی.
یه اصطلاح مهم اینجا هست که باید بدونی: «recertification». این یعنی «دوباره مورد تأیید قرار دادن»؛ قبلا اگه یه تغییر کوچیک می‌دادی باید کل کتاب (یا همون مجموعه برنامه و اثبات‌ها) رو دوباره تأیید و چک می‌کردی. حالا با داستان attach-stobj دیگه این دردسر رو نداری.
توی این مقاله، خلاصه‌ای از این قابلیت attach-stobj داده شده؛ کلی توضیح داده چطوری کار می‌کنه، چه جوری می‌تونی ازش تو برنامه‌هات استفاده کنی، و حتی نکات فنی درباره پیاده‌سازیش گفته شده واسه کسایی که خیلی عمیق دوست دارن ماجرا رو بفهمن.
در کل، قضیه اینه که حالا راحت‌تر میشه یه شی (همون stobj) داشت که توش مدل‌های مختلف با کلی رفتار متفاوت پیاده کنی و لازم نباشه هی بابت بازبینی‌های خسته‌کننده و دوباره‌کاری استرس داشته باشی. خلاصه واسه برنامه‌نویس‌ها و کسایی که با بهینگی و سرعت و تست نرم‌افزار سروکار دارن، این حرکت جدید توی ACL2 کلی می‌تونه کار راه‌انداز باشه!
پس اگه طرفدار ابزارهای خفن چک برنامه هستی یا دوست داری تو دنیای اثبات رسمی (یعنی همون کار با ریاضیات برای مطمئن‌شدن از درستی برنامه)، ACL2 و این رفتار جدیدش رو از دست نده!
منبع: +
