Кіріспе

Жоғары реттік логикалық (HOL) автоматтандырылған теореманы дәлелдеуші

Изабелл автоматтандырылған теореманы дәлелдеуші – жоғары реттік логикалық (HOL) теореманы дәлелдеуші, Стандартты ML және Scala тілдерінде жазылған. LCF стиліндегі теореманы дәлелдеуші ретінде, ол дәлелдемелердің сенімділігін арттыру үшін шағын логикалық ядроға (негізге) негізделген, бірақ нақты дәлелдеме нысандарын қажет етпейді. Изабелл логикалық тұрғыдан қауіпсіз кеңейтулерге мүмкіндік беретін икемді жүйелік аяда қолжетімді, оған теориялар, сондай-ақ кодты құру, құжаттама және әртүрлі формальды әдістерді қолдау үшін жүзеге асырулар кіреді. Оны формальды әдістерге арналған IDE ретінде қарастыруға болады. Соңғы жылдары көптеген теориялар мен жүйелік кеңейтулер Формальдық дәлелдемелердің Изабелл мұрағатында (Изабелл AFP) жинақталды.

Изабелл аты Герард Хьюеттің қызының құрметіне Лоренс Полсонмен берілген. Изабелл теореманы дәлелдеуші – ашық кодты бағдарламалық қамтамасыз ету, қайта қарастырылған BSD лицензиясы бойынша таратылады.

Ерекшеліктері

Изабелл – жалпы мақсаттағы құрал: ол мета-логиканы (әлсіз типтер теориясы) ұсынады, ол бірінші реттік логика (FOL), жоғары реттік логика (HOL) немесе Зермело-Франкель жиыны теориясы (ZFC) сияқты объект логикасын кодтау үшін қолданылады. Ең көп қолданылатын объект логикасы – Isabelle/HOL, бірақ жиыны теориясының маңызды жетістіктері Isabelle/ZF-те орындалды. Изабелдің негізгі дәлелдеу әдісі – жоғары реттік біріктіруге негізделген шешімнің жоғары реттік түрі. Интерактивті болғанымен, Изабеллде тиімді автоматты қорыту құралдары бар, мысалы, термин қайта жазу машинасы және кестелік дәлелдеуші, әртүрлі шешім қабылдау процедуралары және Sledgehammer дәлелдеу автоматтандыру интерфейсі арқылы сыртқы теориялар бойынша қанағаттандырушылық (SMT) шешуіштері (CVC4 кіретін) және шешімге негізделген автоматты теорема дәлелдеуіштері (ATP) – E, SPASS және Vampire (Metis дәлелдеу әдісі осы ATP-лермен жасалған шешім дәлелдемелерін қайта құрайды). Сондай-ақ, екі модель іздеуші (қарсы мысал генераторлары) бар: Nitpick және Nunchaku. Изабеллде үлкен дәлелдемелерді құрылымдауға арналған локальдер бар, олар модульдер болып табылады. Локаль белгілі бір ауқымда типтерді, тұрақтыларды және болжамдарды бекітеді. 2009 жылы NICTA-дағы L4. verified жобасы жалпы мақсаттағы операциялық жүйе ядросының функционалдық дұрыстығының алғашқы ресми дәлелін жасады: seL4 (қауіпсіз кіріктірілген L4) микроядросы. Дәлел Isabelle/HOL-де құрастырылып, тексерілді және C-нің 7500 жолын тексеру үшін 200 000-нан астам жолдан тұратын дәлелдеу скриптін қамтиды. Тексеру кодты, жобалауды және іске асыруды қамтиды, ал негізгі теорема C коды ядроның ресми спецификациясын дұрыс іске асырады деп мәлімдейді. Дәлелдеу seL4 ядросының C кодының ерте нұсқасында 144 қате және жобалау мен спецификациядағы 150-ге жуық мәселені анықтады. Жеңіл Java бағдарламалау тілінің анықтамасы Isabelle-де типтік қауіпсіздігі дәлелденді. Ларри Полсон Изабеллді пайдаланатын зерттеу жобаларының тізімін жүргізеді.