جدول پیوندها
1 مقدمه
2 لینک رقص
3 زبان برنامه نویسی Rust
4 RAC: تضمین مشترک سخت افزار/نرم افزار در مقیاس
5 زنگ و RAR
5.1 زنگ الگوریتمی محدود
6 پیوند رقص در Rust و 6.1 تعاریف
6.2 ترجمه به ACL2
6.3 قضایای پیوندهای رقص
7 کارهای مرتبط
8 نتیجه گیری
9 قدردانی و مراجع
“پیوندهای رقص” بهینه سازی را برای پیاده سازی ساختار داده لیست با پیوند دوگانه دایره ای نشان می دهد که حذف و بازیابی سریع عناصر لیست را فراهم می کند. بهینهسازی Dancing Links عمدتاً در الگوریتمهای سریع برای یافتن جلدهای دقیق مورد استفاده قرار میگیرد و توسط Knuth در جلد 4B از مجموعه اصلی خود به نام هنر برنامهنویسی کامپیوتری رایج شده است. ما پیادهسازی بهینهسازی Dancing Links را در زبان برنامهنویسی Rust و همچنین تأیید رسمی آن با استفاده از اثبات قضیه ACL2 توصیف میکنیم. Rust در چند سال گذشته بهعنوان جانشینی مدرن و ایمن برای C/C++ در شرکتهایی مانند آمازون، گوگل و مایکروسافت مورد تایید قرار گرفته است و در هستههای سیستم عامل لینوکس و ویندوز ادغام میشود. علاقه ما به Rust از پتانسیل آن به عنوان یک زبان تضمین مشترک سخت افزار/نرم افزار با کاربرد در سیستم های حیاتی ناشی می شود. ما زیر مجموعه Rust را با الهام از Russinoff’s Restricted ساخته ایم…