ACL2
 | |
| Парадигма | Функциональный , мета |
|---|---|
| Разработано | Роберт С. Бойер , Дж. Стротер Мур и Мэтт Кауфманн |
| Разработчик | Мэтт Кауфманн и Джей Стротер Мур |
| Впервые появился | 1990 [1] (ограниченное распространение), 1996 (публичное распространение) |
| Стабильная версия | 8,5 / июль 2022 г. |
| Дисциплина набора текста | Динамический |
| ТЫ | Кросс-платформенный |
| Лицензия | БСД |
| Веб-сайт | www |
| Под влиянием | |
| Общий Лисп , Nqthm | |
ACL2 ( A Computational Logic for Applicative Common Lisp ) — программная система, состоящая из языка программирования , расширяемой теории в логике первого порядка и автоматизированного средства доказательства теорем . ACL2 предназначен для поддержки автоматического рассуждения в индуктивных логических теориях, в основном для проверки программного и аппаратного обеспечения . Язык ввода и реализация ACL2 написаны на Common Lisp . ACL2 — бесплатное программное обеспечение с открытым исходным кодом .
Обзор [ править ]
Язык программирования ACL2 является аппликативным ( без побочных эффектов ) вариантом Common Lisp. ACL2 не типизирован. ACL2 Все функции являются тотальными , то есть каждая функция сопоставляет каждый объект в юниверсе ACL2 с другим объектом в его юниверсе.
ACL2 аксиоматизирует семантику Базовая теория языка программирования и встроенных функций. Пользовательские определения на языке программирования, удовлетворяющие принципу определений, расширяют теорию таким образом, чтобы поддерживать ее логическую последовательность .
Ядро средства доказательства теорем ACL2 основано на переписывании терминов , и это ядро можно расширять, поскольку обнаруженные пользователем теоремы могут использоваться в качестве специальных доказательства методов для последующих гипотез .
ACL2 задуман как «промышленная» версия средства доказательства теорем Бойера-Мура, NQTHM . Для достижения этой цели ACL2 имеет множество функций для поддержки чистого проектирования интересных математических и вычислительных теорий. ACL2 также повышает эффективность благодаря построению на Common Lisp; например, та же спецификация, которая является основой для индуктивной проверки, может быть скомпилирована и запущена в исходном виде .
В 2005 году авторы семейства средств доказательства Бойера-Мура, в которое входит ACL2, получили премию ACM Software System Award «за новаторство и разработку наиболее эффективного средства доказательства теорем (...) в качестве инструмента формальных методов для проверки критически важного с точки зрения безопасности оборудования. и программное обеспечение». [2] [3]
Доказательства [ править ]
ACL2 нашел множество промышленных применений. [4] [5] В 1995 году Дж. Стротер Мур , Мэтт Кауфманн и Том Линч использовали ACL2, чтобы доказать правильность операции деления с плавающей запятой микропроцессора AMD K5 после ошибки Pentium FDIV . [6]
Промышленными пользователями ACL2 являются AMD, Arm, Centaur Technology, IBM, Intel, Oracle и Collins Aerospace.
См. также [ править ]
Ссылки [ править ]
- ^ «XDOC — Примечание-1-7» . www.cs.utexas.edu .
- ^ «ACM: Пресс-релиз, 15 марта 2006 г.» . 1 августа 2008 г. Архивировано из оригинала 1 августа 2008 г.
- ^ «Премия программной системы» . Награды АКМ . Ассоциация вычислительной техники . Архивировано из оригинала 02 апреля 2012 г. Проверено 14 января 2012 г.
- ^ «Аннотированная библиография ACL2» . www.cs.utexas.edu .
- ^ «Семинары ACL2 и семинар UT ACL2» . www.cs.utexas.edu .
- ^ Мур, Дж. Стротер; Линч, Том; Кауфманн, Мэтт (1996). «Механически проверенное доказательство корректности ядра алгоритма деления с плавающей запятой AMD5K86». Транзакции IEEE на компьютерах . 47 . CiteSeerX 10.1.1.43.3309 .