Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
ACL2 (A Computational Logic for Applicative Common Lisp) – это программная система, состоящая из языка программирования, расширяемой теории в логике первого порядка и автоматического доказателя теорем. ACL2 разработан для поддержки автоматизированного рассуждения в индуктивных логических теориях, главным образом для верификации программного и аппаратного обеспечения. Язык ввода и реализация ACL2 написаны на Common Lisp. ACL2 является свободным программным обеспечением с открытым исходным кодом.
Programming language and theorem prover
ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open source software.
Обзор
Язык программирования ACL2 является аппликативным (не имеющим побочных эффектов) вариантом Common Lisp. ACL2 не имеет строгой типизации. Все функции ACL2 являются тотальными, то есть каждая функция отображает каждый объект во вселенной ACL2 в другой объект этой же вселенной. Базовая теория ACL2 аксиоматизирует семантику языка программирования и его встроенных функций. Пользовательские определения в языке программирования, удовлетворяющие принципу определимости, расширяют теорию таким образом, чтобы сохранить её логическую непротиворечивость. Ядро доказателя теорем ACL2 основано на переписывании термов, и это ядро расширяемо: теоремы, открытые пользователями, могут использоваться как ad hoc методы доказательства для последующих утверждений. ACL2 задуман как версия теоремы Бойера — Мура, NQTHM, обладающая «индустриальной надёжностью». С этой целью ACL2 имеет множество средств, поддерживающих разработку интересных математических и вычислительных теорий с соблюдением принципов чистого проектирования. ACL2 также выигрывает в эффективности благодаря тому, что построен на Common Lisp: например, одна и та же спецификация, лежащая в основе индуктивной верификации, может быть скомпилирована и запущена непосредственно. В 2005 году авторы семейства систем доказательства теорем Boyer — Moore, в которое входит ACL2, получили премию ACM Software System Award «за новаторскую разработку и создание высокоэффективного доказателя теорем ( ) как инструмента формальных методов для верификации критически важных аппаратных и программных средств».
The ACL2 programming language is an applicative (side effect free) variant of Common Lisp. ACL2 is untyped. All ACL2 functions are total — that is, every function maps each object in the ACL2 universe to another object in its universe. ACL2's base theory axiomatizes the semantics of its programming language and its built in functions. User definitions in the programming language that satisfy a definitional principle extend the theory in a way that maintains the theory's logical consistency. The core of ACL2's theorem prover is based on term rewriting, and this core is extensible in that user discovered theorems can be used as ad hoc proof techniques for subsequent conjectures. ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, NQTHM. Toward this goal, ACL2 has many features to support clean engineering of interesting mathematical and computational theories. ACL2 also derives efficiency from being built on Common Lisp; for example, the same specification that is the basis for inductive verification can be compiled and run natively. In 2005, the authors of the Boyer Moore family of provers, which includes ACL2, received the ACM Software System Award "for pioneering and engineering a most effective theorem prover ( ) as a formal methods tool for verifying safety critical hardware and software."
Доказательства
ACL2 нашла широкое применение в промышленности. В 1995 году J. Strother Moore, Matt Kaufmann и Tom Lynch использовали ACL2 для доказательства корректности операции деления чисел с плавающей точкой в микропроцессоре AMD K5 после обнаружения ошибки Pentium FDIV. Обзор некоторых применений системы представлен на странице "Интересные приложения" в документации ACL2. Среди промышленных пользователей ACL2 — компании AMD, Arm, Centaur Technology, IBM, Intel, Oracle и Collins Aerospace.
ACL2 has had numerous industrial applications. In 1995, J Strother Moore, Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of the AMD K5 microprocessor in the wake of the Pentium FDIV bug. The interesting applications page of the ACL2 documentation has a summary of some uses of the system. Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.