Компьютерные логические построения: подход

Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Kluwer Academic Publishers, June, 2000. (ISBN 0-7923-7744-3)


Описание

Эта книга — учебник-введение в компьютерную логику. Он подходит для выпускников и студентов, изучающих углубленную программу по направлениям «Разработка программного обеспечения» и «Формальные методы». В сочетании с другими книгами учебник подходит для курсов «Разработка аппаратного обеспечения», «Дискретная математика» и «Теория», в частности для курсов, где важны формальная логика, точность или автоматизированная поддержка. Он также подходит для курсов по Искусственному интеллекту и Автоматизированным логическим построениям.

Современные системы аппаратного и программного обеспечения часто очень сложны, и отмечается тенденция к еще большему усложнению. При помощи математического моделирования систем мы получаем модели с гарантированно корректным поведением. Чтобы дополнительно убедиться в точности рассуждений (которые могут быть довольно сложными), мы можем использовать компьютерную программу, которая проверит наши доказательства. Мы даже можем автоматизировать некоторые построения.

В этой книге представлены:

  • Практический функциональный язык программирования, тесно связанный с Common Lisp, который используется для определения функций (которые способны смоделировать вычислительные системы) и выдачи суждений об определенных функциях.
  • Формальная логика, в которой определенные функции соответствуют аксиомам; логика первого порядка включает индукцию и позволяет нам доказывать теоремы о функциях.
  • Система автоматизированных рассуждений ACL2, включающая язык программирования, логику и механизированную поддержку процесса доказательства.

Эта книга научит вас формализовать понятия, конструировать доказательства и использовать автоматические инструменты для проверки доказательств.

Мы используем определенную формализацию и автоматизацию, а именно ACL2, которая находится в свободном доступе и распространяется по условиям лицензии на основе BSD через сайт ACL2. ACL2 была написана Кауфманом и Муром, и фактически наследует «Доказательство теорем Бойера-Мура» Nqthm. (Боб Бойер также внес значительный вклад в ACL2 на ранних этапах.) На домашней странице ACL2 доступно онлайн-руководство, которое представляет собой большой гипертекстовый документ, предназначенный в первую очередь для пользователей системы. Эта книга — полное введение в ACL2, включающее описание работы с системой.

При обучении использованию автоматизированной формализации мы фокусируемся на вычислительных проблемах, с которыми обычно сталкиваются те, кто использует формальные методы для анализа аппаратного и программного компьютерного обеспечения.

ACL2 используется в промышленности. Помните баг Intel FDIV? Первый Pentium [торговая марка, принадлежит Intel, Inc] не способен правильно делить числа с плавающей запятой, исправление ошибки стоило Intel $500 миллионов. После этого случая мы использовали ACL2, чтобы подтвердить, что микрокод деления чисел с плавающей запятой в конкурирующем микропроцессоре AMD, AMD-K5, работает корректно. AMD использовали ACL2 для подтверждения элементарных операций над числами с плавающей точкой для недавно выпущенного Athlon. [Примечания: AMD, логотип AMD и их комбинации, AMD-K5, AMD-K7 и AMD Athlon являются торговыми марками, принадлежащими Advanced Micro Devices, Inc.] Сопутствующая книга содержит тесно связанное изучение случая.

Система ACL2 успешно применялась в коммерческих проектах, в том числе при моделировании микропроцессоров, проверке работы аппаратного обеспечения, микрокода и программного обеспечения. Эта книга предоставляет методологию для формального моделирования вычислительных систем, а также для логического анализа этих моделей с использованием автоматизации. Практичность компьютерных логических построений подробнее демонстрируется в сопутствующей книге Компьютерные логические построения: изучение примеров использования ACL2.


Опечатки

Все ошибки, отмеченные ниже, были исправлены в печатной версии книги, распространяемой lulu (смотрите Информацию для заказа). Однако если у вас версия в твердом переплете от Волтерс Клувер или не самое последнее издание печатной версии, заметки ниже могут пригодиться.

Для удобства читателей всех последних версий мы расположили ошибки двумя способами.

Во-первых, обычно мы указываем раздел, параграф и номер предложения, в котором найдена ошибка. В рукописи первый параграф каждого раздела идет без отступа, все остальные параграфы даны с отступом. Мы считаем параграфы с 1. Текст, повторяющий дисплей (например, формулы или перечисления), не считается новым параграфом, кроме случаев, когда он отделен отступом. Предложения оканчиваются точкой и считаются от 1.

Второй маркер ошибки — номер страницы и строки в издании с твердым переплетом от Волтерс Клувер. Обычно каждая страница издания начинается заголовком, включающим номер страницы, название книги или главы, а также горизонтальную линию шириной во всю страницу. Мы считаем все не пустые линии под горизонтальной чертой (например, мы не считаем сам заголовок, но считаем все последующие заполненные строки, будь они частью названия раздела, текстом с дисплея или обычным текстом). Страницы и строки издания в твердом переплете могут не соответствовать таковым в других изданиях.

  • Раздел 3.2.1, параграф 6, предложение 1; Волтерс Клувер, страница 33, строка 6: вместо фразы ``a ACL2 object'' должно быть ``an ACL2 object''.
  • Раздел 3.2.1, параграф 19, предложение 2; Волтерс Клувер, страница 35, строка 8, после Рисунка 3.2: вместо ``a ACL2 object'' должно быть ``an ACL2 object''.
  • Раздел 4.3, параграф 4, экран после предложения 1; Волтерс Клувер, страница 61, строки 29 и 30: два проигнорированных сообщений сборщика мусора нужно читать как
    [SGC for 86 FIXNUM pages .. ... GC finished]
    Отображенный текст содержит LaTeX для создания эллипса.
  • Раздел 6.2, параграф 3, предложение 2; Волтерс Клувер, страница 83, строка 20: предложение

    Analogously, (or p1 p2 ...) <==> (if p1 t (or p2 ...)), where (or p1) abbreviates p1.

    нужно читать как

    Analogously, (or p1 p2 ...) <==> (if p1 p1 (or p2 ...)), where (or p1) abbreviates p1.

  • Раздел 7.3, параграф 5, предложение 1; Волтерс Клувер, страница 109, строка 18: ``where size in measured'' нужно читать как ``where size is measured''.
  • Раздел 8.3.3, параграф 7 (который начинается с заголовка Types), предложение 4; Волтерс Клувер, страница 145, строка -3 (третья строка снизу): ``{0}, {nil}, and {t}'' нужно читать как ``{0}, {nil}, and {t}.'' Предложение должно оканчиваться точкой.
  • Раздел 8.2; Волтерс Клувер, страница 122: В некоторых версиях печатного издания есть ссылка на Рисунок 8.1, но само изображение отсутствует. Рисунок 8.2 такой же, как Рисунок 2.1, который есть в Разделе 2.5 в изданиях с мягким переплетом.
  • Раздел 10.6; Волтерс Клувер, страница 203: В версиях ACL2 старше 2.9 мы начали соблюдать дополнительные ограничения на имена пакетов, а именно: использование строчных букв больше не допускается. В связи с этим нам пришлось изменить имя пакета, использованного в примере в Разделе 10.6, с "compile" на "COMPILE". Изменения нужно сделать в трех местах.
  • (1) Параграф 2, предложение 3; Волтерс Клувер, страница 203, строка 35: команда, которая начинается с

    (defpkg "compile"

    должна начинаться с

    (defpkg "COMPILE"

    (2) Параграф 3, предложение 4; Волтерс Клувер, страница 204, строка 8: вместо фразы

    The above defpkg defines the new symbol package compile

    должно быть

    The above defpkg defines the new symbol package COMPILE

    (3) Параграф 3, после предложения 4; Волтерс Клувер, страница 204, строка 11: вместо команды

    (in-package "compile")

    должна быть

    (in-package "COMPILE")

  • Раздел 11.1, Упражнение 11.2; Волтерс Клувер, страница 211, последняя строка на странице: Упражнение 11.2 ссылается на страницы 49 и 115. Правильные ссылки в издании Волтерс Клувер - страницы 107 и 115.
  • Раздел 11.2, Упражнение 11.5; Волтерс Клувер, страница 213, строка 4: не хватает ``)'' в конце пункта, который начинается с ``Use :trans1 to print ...''
  • Раздел 11.7, Упражнение 11.49; Волтерс Клувер, страница 220, строка 5: Упражнение 11.49 просто неправильное. Формула, которая якобы не является теоремой, на самом деле теорема, потому контр-пример привести невозможно! То, что мы имели в виду, не имеет ничего общего с обменной сортировкой слиянием mergesort, но является наблюдением за количеством (perm, how-many) и квантификацией. Упражнение должно было быть таким:

    Exercise 11.49 The following is a theorem in a suitable logic permitting ACL2 terms and first-order quantification.

      (perm a b)
    <->
      (ALL e (equal (how-many e a)
                    (how-many e b)))
    

    Here, by ALL we mean the universal quantifier conventionally written with an upside down A. The universal quantifier in the above theorem is crucial! The similar looking ACL2 formula

    (iff (perm a b)
         (equal (how-many e a)
                (how-many e b)))
    

    is not a theorem. Exhibit a counterexample.


Оригинал: http://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html

Домашняя страница