Jump to content

ACL2

ACL2
Парадигма Функциональный , мета
Разработано Роберт С. Бойер , Дж. Стротер Мур и Мэтт Кауфманн
Разработчик Мэтт Кауфманн и Джей Стротер Мур
Впервые появился 1990 [1] (ограниченное распространение), 1996 (публичное распространение)
Стабильная версия
8,5 / июль 2022 г. ( 2022-07 )
Дисциплина набора текста Динамический
ТЫ Кросс-платформенный
Лицензия БСД
Веб-сайт www .cs .utexas .edu /пользователи /мур /acl2
Под влиянием
Общий Лисп , 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.

См. также [ править ]

Ссылки [ править ]

  1. ^ «XDOC — Примечание-1-7» . www.cs.utexas.edu .
  2. ^ «ACM: Пресс-релиз, 15 марта 2006 г.» . 1 августа 2008 г. Архивировано из оригинала 1 августа 2008 г.
  3. ^ «Премия программной системы» . Награды АКМ . Ассоциация вычислительной техники . Архивировано из оригинала 02 апреля 2012 г. Проверено 14 января 2012 г.
  4. ^ «Аннотированная библиография ACL2» . www.cs.utexas.edu .
  5. ^ «Семинары ACL2 и семинар UT ACL2» . www.cs.utexas.edu .
  6. ^ Мур, Дж. Стротер; Линч, Том; Кауфманн, Мэтт (1996). «Механически проверенное доказательство корректности ядра алгоритма деления с плавающей запятой AMD5K86». Транзакции IEEE на компьютерах . 47 . CiteSeerX   10.1.1.43.3309 .

Внешние ссылки [ править ]

Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: a1c0c391947ee4e5d99f1090b2e78dde__1717260000
URL1:https://arc.ask3.ru/arc/aa/a1/de/a1c0c391947ee4e5d99f1090b2e78dde.html
Заголовок, (Title) документа по адресу, URL1:
ACL2 - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)