Комп’ютерне мислення: підхід

Source: https://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html

Метт Кауфманн, Панагіотіс Маноліос і Дж. Стротер Мур, Kluwer Academic Publishers, червень 2000 р. (ISBN 0-7923-7744-3)

• опис
• Зміст і витяги (pdf .2Mb) (ps .8Mb) .
• Додатки («Використання системи ACL2», «Додаткові функції»), Бібліографія та покажчик (pdf)
• Виправлення
• Рішення до вправ
• Інформація про замовлення

Опис

Ця книга є вступним посібником до комп’ютерного логічного мислення. Його можна використовувати в аспірантурі та студентах вищих відділень з розробки програмного забезпечення або формальних методів. Він також підходить у поєднанні з іншими книгами в курсах з дизайну апаратного забезпечення, дискретної математики або теорії, особливо курсів, які підкреслюють формалізм, точність або механізовану підтримку. Він також підходить для курсів зі штучного інтелекту або автоматизованого міркування.

Сучасні апаратні та програмні системи часто є дуже складними, і тенденція до підвищення складності. Моделюючи системи математично, ми отримуємо моделі, правильну поведінку яких ми можемо довести. Щоб ще більше підвищити довіру до наших міркувань, які можуть бути складними, ми можемо використовувати комп’ютерну програму для перевірки наших доказів і навіть для автоматизації деяких їх побудов.

У цій книзі ми представляємо:

• Практична функціональна мова програмування, тісно пов’язана з 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 була успішно застосована в проектах комерційного інтересу, включаючи моделювання мікропроцесора, перевірку апаратного забезпечення, перевірку мікрокоду та перевірку програмного забезпечення. У цій книзі представлено методологію формального моделювання обчислювальних систем і міркувань про ці моделі за допомогою механізованої допомоги. Практичність комп’ютерних міркувань додатково демонструється в супровідній книзі Computer-Aided Reasoning: ACL2 Case Studies.