Bilgisayar Destekli Muhakeme: Bir Yaklaşım

The source-page: http://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html

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

Açıklama

Bu kitap, bilgisayar destekli muhakeme ders kitabıdır. Yazılım Mühendisliği veya Formel Metotlar üzerine lisansüstü ve üst bölüm lisans derslerinde kullanılabilir. Ayrıca Donanım Tasarımı, Ayrık Matematik veya Teori derslerinde, özellikle formalizmi, titizliği veya mekanize desteği vurgulayan derslerde diğer kitaplarla birlikte de uygundur. Yapay Zeka ve Otomatik Muhakeme dersleri için de uygundur.

Mevcut donanım ve yazılım sistemleri genellikle çok karmaşıktır ve eğilim artan karmaşıklığa yöneliktir. Sistemleri matematiksel olarak modelleyerek, doğru davranabileceğini kanıtlayabileceğimiz modeller elde ediyoruz. İhtiyacımız olan karmaşık olan güvenimizi daha da artırmak için, kanıtlarımızı kontrol etmek ve hatta bazılarını otomatikleştirmek için bir bilgisayar programı kullanabiliriz.

Bu kitapta sunduğumuz:

  • İşlevleri tanımlamak (bilgisayar sistemlerini modelleyebilen) ve tanımlanmış işlevler hakkında iddialarda bulunmak için kullanılan Common Lisp ile yakından ilgili pratik bir işlevsel programlama dili.
  • Tanımlanmış fonksiyonların aksiyomlara karşılık geldiği biçimsel bir mantık; mantık birinci derecedir, indüksiyon içerir ve fonksiyonlarla ilgili teoremleri kanıtlamamızı sağlar.
  • Programlama dilini, mantığı ve prova işlemi için mekanik desteği içeren bilgisayar destekli muhakeme sistemi ACL2.

Bu kitap size nasıl bir şeylerin resmileştirileceğini, provaların nasıl yapılacağını ve bu provaları kontrol etmek için mekanik bir aracın nasıl kullanılacağını öğretecektir.

Biz belirli bir formalizmini ve bir BSD Lisansı şartları altında serbestçe kullanılabilir bunun belirli bir mekanizasyon, yani ACL2 kullanmak ACL2 ana sayfasına. ACL2, Kaufmann ve Moore tarafından yazılmıştır ve “Boyer-Moore teoremi kanıtı” Nqthm’nin halefidir. (Bob Boyer ayrıca ACL2’ye önemli katkılarda bulundu.) ACL2 giriş sayfası, esas olarak sistemin kullanıcıları için kullanılan büyük bir köprü metni belgesi olan çevrimiçi başvuru kılavuzunu içerir. Bu kitap ACL2’ye kesin giriş ve nasıl kullanılacağıdır.

Mekanize formalizmin kullanımını öğretirken, genellikle bilgisayar donanımını veya yazılımını analiz etmek için resmi yöntemleri kullanan birinin karşılaştığı türdeki hesaplama problemlerine odaklanıyoruz.

ACL2 endüstride kullanılır. Intel FDIV hatasını hatırladın mı? İlk Pentium [ticari marka, Intel, Inc] kayan nokta sayılarını doğru şekilde bölemiyordu ve bildirildiği üzere Intel 500 milyon dolara mal oldu. Gerçekleşen zamanda, AMD’nin rakip mikroişlemcisi AMD-K5’in kayan nokta bölmeli mikro kodunun doğru olduğunu doğrulamak için ACL2’yi kullandık. AMD, yakın zamanda piyasaya sürülen Athlon için temel kayan nokta işlemlerini doğrulamak için ACL2’yi kullandı. [Not: AMD, AMD logosu ve bunların kombinasyonları, AMD-K5, AMD-K7 ve AMD Athlon, Advanced Micro Devices, Inc.’in ticari markalarıdır.] Arkadaş hacim bir yakından ilişkili çalışması sunmaktadır.

ACL2 sistemi, mikroişlemci modellemesi, donanım doğrulama, mikro kod doğrulama ve yazılım doğrulama dahil ticari ilgi alanlarına başarıyla uygulanmıştır. Bu kitap, bilgisayar sistemlerini resmi olarak modellemek ve mekanize yardımı olan modeller hakkında muhakeme için bir metodoloji sunmaktadır. Bilgisayar destekli muhakemenin pratikliği kitapta ayrıca gösterilmiştir, Bilgisayar Destekli Muhakeme: ACL2 Vaka Çalışmaları.