تأیید رسمی و دستیاران اثبات
تأیید رسمی، با استفاده از اثبات ریاضی بررسیشده توسط ماشین، نشان میدهد که نرمافزار با مشخصات خود مطابقت دارد؛ دستیاران اثبات ابزارهایی هستند که چنین اثباتهایی را میسازند و بررسی میکنند.
Definition
تأیید رسمی عبارت است از ساخت یک اثبات دقیق و بررسیشده توسط ماشین که یک سیستم مشخصات رسمی را برآورده میکند، و دستیار اثبات نرمافزاری است که به کاربر کمک میکند چنین اثباتهایی را توسعه دهد و اعتبار آنها را به صورت مکانیکی بررسی کند.
Scope
این موضوع شامل تأیید استنتاجی و اثبات قضیه تعاملی است: دستیاران اثبات مبتنی بر نظریه نوع یا منطق مرتبه بالاتر (مانند Coq، Isabelle، Lean و Agda)، رویکرد LCF برای اثبات قابل اعتماد، مبنای گزارهها به عنوان انواع، خودکارسازی اثبات و تاکتیکها، و مصنوعات تأیید شده برجسته از جمله کامپایلرها و هستههای سیستم عامل.
Core questions
- چگونه میتوان صحت عملکرد کامل را اثبات و توسط ماشین بررسی کرد؟
- چرا دستیاران اثبات قابل اعتماد هستند و پایگاه محاسباتی قابل اعتماد چیست؟
- مکاتبه کوری-هاوارد چگونه اثباتها و برنامهها را به هم متصل میکند؟
- چه چیزی برای تأیید سیستمهای واقعی مانند کامپایلرها و هستهها لازم است؟
Key theories
- رویکرد LCF برای اثبات قابل اعتماد
- Edinburgh LCF گوردون، میلنر و وادزورث یک هسته اثبات قابل اعتماد کوچک را معرفی کرد که تمام قضایا باید از آن عبور کنند، به طوری که حتی خودکارسازی پیچیده نیز نمیتواند اثباتهای نادرست تولید کند.
- کامپایلر تأیید شده (CompCert)
- CompCert لروی یک کامپایلر C است که صحت آن در یک دستیار اثبات، با یک قضیه بررسیشده توسط ماشین که کد تولید شده معناشناسی برنامه منبع را بهبود میبخشد، اثبات شده است.
- هسته سیستم عامل تأیید شده (seL4)
- کلاین و همکارانش یک اثبات بررسیشده توسط ماشین از صحت عملکردی برای میکروکرنل seL4 تولید کردند که تأیید سرتاسری نرمافزار سیستمهای سطح پایین را نشان میدهد.
Clinical relevance
تأیید مکانیزه بالاترین اطمینان موجود را برای نرمافزارهای حیاتی فراهم میکند و کامپایلرها، هستهها و کتابخانههای رمزنگاری را با ضمانتهای اثباتشده به جای اطمینان مبتنی بر آزمایش تولید میکند. دستیاران اثبات به طور فزایندهای برای رسمیسازی خود ریاضیات نیز استفاده میشوند.
History
اثبات قضیه تعاملی با Edinburgh LCF در دهه 1970 آغاز شد، که زبان فرا ML و هسته قابل اعتماد آن سیستمهای بعدی را شکل داد. دستیاران مبتنی بر نظریه نوع مانند Coq و Agda و سیستمهای منطق مرتبه بالاتر مانند Isabelle/HOL در دهههای بعدی به بلوغ رسیدند و به مصنوعات تأیید شده برجسته منجر شدند: کامپایلر CompCert (2009) و هسته seL4 (2009).
Debates
- هزینه تأیید در مقابل اطمینان به دست آمده
- ساخت اثباتهای بررسیشده توسط ماشین برای سیستمهای بزرگ نیازمند تلاش عظیمی است، که بحثهایی را در مورد اینکه تأیید کامل در کجا توجیه میشود در مقابل جایی که روشهای سبکتر کافی هستند، و چقدر اثبات میتواند خودکار شود، برانگیخته است.
Key figures
- Robin Milner
- Michael Gordon
- Xavier Leroy
- Gerwin Klein
- Robert Harper
Related topics
Seminal works
- gordon1979
- leroy2009
- klein2009
- harper2016
Frequently asked questions
- دستیار اثبات چیست؟
- دستیار اثبات نرمافزاری است که در آن کاربر به صورت تعاملی اثباتهای رسمی را میسازد در حالی که سیستم هر مرحله را به صورت مکانیکی بررسی میکند، به طوری که یک اثبات تکمیل شده تا یک هسته کوچک و به خوبی بررسی شده قابل اعتماد است.
- تأیید یک برنامه چه تفاوتی با آزمایش آن دارد؟
- آزمایش رفتار را بر روی ورودیهای انتخاب شده بررسی میکند و تنها میتواند وجود اشکالات را آشکار کند، در حالی که تأیید رسمی صحت را برای تمام ورودیهای مجاز توسط مشخصات اثبات میکند و عدم وجود خطاهای مشخص شده را تأیید میکند.