ACL2 - ACL2

ACL2
ACL2 Logo 2014 transparent.png
ПарадигмаФункциональный, мета
РазработаноРоберт С. Бойер, Дж. Стротер Мур и Мэтт Кауфманн
РазработчикМэтт Кауфманн и Дж. Стротер Мур
Впервые появился1990 (ограниченное распространение), 1996 (публичное распространение)
Стабильный выпуск
8.2 / май 2019 (2019-05)
Печатная дисциплинаДинамический
Операционные системыКроссплатформенность
ЛицензияBSD
Интернет сайтwww.cs.utexas.edu/ пользователи/ Мур/ acl2
Под влиянием
Common Lisp, Nqthm

ACL2 («Вычислительная логика для аппликативного 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 «за новаторство и разработку наиболее эффективного средства доказательства теорем (...) в качестве формального инструмента для проверки критически важного для безопасности оборудования и программного обеспечения».[1][2]

Доказательства

ACL2 имеет множество промышленных применений.[3][4] В 1995 г. Дж. Стротер Мур, Мэтт Кауфманн и Том Линч использовал ACL2, чтобы доказать правильность операции деления с плавающей запятой AMD K5 микропроцессор вслед за Ошибка Pentium FDIV.[5] В интересные приложения На странице документации ACL2 есть краткое описание некоторых применений системы.

Промышленные пользователи ACL2 включают AMD, Arm, Centaur Technology, IBM, Intel, Oracle и Rockwell Collins.

использованная литература

  1. ^ ACM: пресс-релиз, 15 марта 2006 г.
  2. ^ «Премия за программные системы». ACM Awards. Ассоциация вычислительной техники. Архивировано из оригинал на 2012-04-02. Получено 14 января, 2012.
  3. ^ Книги и статьи о ACL2 и его приложениях
  4. ^ Серия семинаров ACL2
  5. ^ «Механически проверенное доказательство правильности ядра алгоритма деления с плавающей запятой AMD5K86». CiteSeerX  10.1.1.43.3309. Цитировать журнал требует | журнал = (Помогите)

внешние ссылки