Введение

Автоматизированный теоремадоказатель логики высшего порядка (HOL)

Автоматизированный теоремадоказатель Isabelle – это теоремадоказатель логики высшего порядка (HOL), написанный на языках Standard ML и Scala. Являясь теоремадоказателем в стиле LCF, он основан на небольшом логическом ядре (kernel), что повышает надёжность доказательств, не требуя при этом поддержки явных объектов доказательств. Isabelle доступна в рамках гибкой системной структуры, позволяющей создавать логически безопасные расширения, включающие как теории, так и реализации для генерации кода, документации и специализированной поддержки различных формальных методов. Его можно рассматривать как интегрированную среду разработки (IDE) для формальных методов. За последние годы значительное количество теорий и системных расширений было собрано в Архиве формальных доказательств Isabelle (Isabelle AFP).

Название Isabelle было дано Лоуренсом Полсоном в честь дочери Жерара Хюэ. Автоматизированный теоремадоказатель Isabelle является свободным программным обеспечением, распространяемым по пересмотренной лицензии BSD.

Особенности

Изабель является универсальной: она предоставляет металогику (слабую теорию типов), которая используется для кодирования объектных логик, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Наиболее широко используемой объектной логикой является Isabelle/HOL, хотя значительные разработки в теории множеств были завершены в Isabelle/ZF. Основным методом доказательства в Isabelle является версия резолюции высшего порядка, основанная на унификации высшего порядка. Несмотря на интерактивность, Isabelle располагает эффективными инструментами автоматического рассуждения, такими как механизм переписывания термов и построитель таблиц, различные процедуры принятия решений, а также, через интерфейс автоматизации доказательств Sledgehammer, внешние решатели задач выполнимости с учетом теорий (SMT) (включая CVC4) и автоматические теоремы доказывания на основе резолюции (ATP), включая E, SPASS и Vampire (метод доказательства Metis реконструирует доказательства резолюции, генерируемые этими ATP). Также имеются два генератора моделей (генераторы контрпримеров): Nitpick и Nunchaku. Isabelle поддерживает локали – модули, структурирующие большие доказательства. Локаль фиксирует типы, константы и предположения в заданной области видимости.

В 2009 году проект L4.verified в NICTA представил первое формальное доказательство функциональной корректности ядра операционной системы общего назначения: микроядра seL4 (защищенное встроенное L4). Доказательство построено и проверено в Isabelle/HOL и состоит из более чем 200 000 строк скрипта доказательства для верификации 7500 строк кода на C. Верификация охватывает код, проектирование и реализацию, а основная теорема утверждает, что код на C правильно реализует формальную спецификацию ядра. В процессе доказательства было обнаружено 144 ошибки в ранней версии кода на C ядра seL4 и около 150 проблем в проектировании и спецификации. Типобезопасность определения языка программирования Lightweight Java была доказана в Isabelle. Ларри Полсон ведет список исследовательских проектов, использующих Isabelle.