Article posted on:May 8, 2024
Article updated on:Aug 30, 2024
This translation is provided by StudyCrumb, a premier assignment assistance company dedicated to helping students achieve their academic dreams. If you're looking for someone to "write my essay for me," our experienced team at StudyCrumb is here to deliver top-notch essays tailored to your specific needs. From complex research papers to persuasive essays, we take the stress out of your assignments, ensuring you receive quality work that meets your expectations and deadlines.
Source: https://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html
Метт Кауфманн, Панагіотіс Маноліос і Дж. Стротер Мур, Kluwer Academic Publishers, червень 2000 р. (ISBN 0-7923-7744-3)
Ця книга є вступним посібником до комп’ютерного логічного мислення. Його можна використовувати в аспірантурі та студентах вищих відділень з розробки програмного забезпечення або формальних методів. Він також підходить у поєднанні з іншими книгами в курсах з дизайну апаратного забезпечення, дискретної математики або теорії, особливо курсів, які підкреслюють формалізм, точність або механізовану підтримку. Він також підходить для курсів зі штучного інтелекту або автоматизованого міркування.
Сучасні апаратні та програмні системи часто є дуже складними, і тенденція до підвищення складності. Моделюючи системи математично, ми отримуємо моделі, правильну поведінку яких ми можемо довести. Щоб ще більше підвищити довіру до наших міркувань, які можуть бути складними, ми можемо використовувати комп’ютерну програму для перевірки наших доказів і навіть для автоматизації деяких їх побудов.
У цій книзі ми представляємо:
Ця книга навчить вас, як формалізувати речі, як будувати докази та як використовувати механічний інструмент для перевірки цих доказів.
Ми використовуємо певний формалізм і його особливу механізацію, а саме 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.