ACL2 Version 4.2 [German]

 

ACL2

 

ACL2 ist eine Programmiersprache mit der man Computersysteme modelieren kann, und ein Tool, das euch hilft  Eigenschaften dieser Modele zu prüfen.

ACL2 ist ein Teil von Boyer-Moore Beweiserfamilie, welche Autoren dafür in 2005 ACM Software System Award bekommen haben.

 

 


Hier starten: Applications, Touren, und Tutorials/Demos ACL2 Workshops und UT ACL2 Seminar
Bücher und Werke über ACL2 und seine Applications User'sLehrbuch und Hyper-Card
Lemma Bibliotheken und Utilities Mailing Listen
Letzte Veränderungen auf der Seite Erlangen und Installing Version 4.2
Unterschiede von Version 4.1 Andere Releasen
Wie trage ich zu Bibliotheken und Dokumentation bei

 

Originalartikel von Matt Kaufmann und J Strother Moore
University of Texas at Austin
January 10, 2011

 


ACL2 Distribution enthält unterschiedliche Extensionen, die von folgenden Personen beigetragen waren.

  • ACL2(r)
    Support von Realen Zahlen mit Hilfe von non-standard Analyse
    Ruben Gamboa
  • ACL2(h)
    Support für hash cons, applikative Hash-Tabellen, und Memoizationfunktion für die Wiederverwendung von bereits berechneten Ergebnissen
    Bob Boyer and Warren A. Hunt, Jr.
  • ACL2(p)
    Support für parallele Abschätzung
    David L. Rager

Die Distribution enthält auch Bibliotheken von books (Files mit Definitionen und Theoremen), die von uns geschriebene Code erweitern. Bücher waren hinzugefügt und sind unterhalten von ACL2 Verein (sieh  http://acl2-books.googlecode.com/) und ihre Autoren sind gewöhnlich in jedem Buch oder in README file erwähnt.

Eine andere Extension von ACL2 ist Eclipse-basierter  ACL2 Sedan (ACL2s). Im Unterschied zu den Systemen oben, ist ACL2s von Pete Manolios und seiner Forschungsgruppe verbreitet und unterhalten. ACL2s kommt mit einem standerten lauffähigen ACL2 Bild für Windows, aber es kommt auch mit pre-certified Büchern und Extension von ACL2 mit zusätzlichen Eigenschaften, inklusive extra Automatisierung für Terminationbeweise und Gegenbeispielgeneration.


Wir sind den folgenden Organisationen für ihre Unterstützung sehr dankbar. (Eine volle Liste kannn man auf der Seite finden acknowledgments page.)

  • DARPA
  • National Science Foundation
    • Dieser Stoff gründet sich auf Arbeit unterstützt von  National Science Foundation unter Grant Nos. EIA-0303609, CNS-0429591, ISS-0417413, CCF-0945316, und CNS-0910913.
    • Alle Meinungen, Entdeckungen, Empfehlungen, die hier zum Ausdruck kommen, gehören den Autoren und stimmen nicht immer mit Meinung von National Science Foundation überein.
  • Advanced Micro Devices, Inc.
  • ForrestHunt, Inc.
  • Rockwell Collins, Inc.
  • Sun Microsystems, Inc.

The User's Manual

ACL2's User Lehrbuch ist ein vast hypertext Dokument. Man kann es hier überfliegen, in HTML Format.

Hier sind zwei Hauptzeilen zum Dokumentationgrafik:

Hauptthemen (Inhaltsverzeichnis)
Liste von allen Themen

Die winzige Warnzeichen, , zeigen darauf, dass die Links aus der Einleitungsebene zur Hinweisanleitung führen. Nachdem alle Links in der Hinweisanleitung sind, führen sie eigentlich in die Anleitung und keine ist mit dem Warnzeichen markiert! Deshalb können die Neuankömmlinge sich leicht verirren.

Hier sind unsere Empfehlungen für die Benutzung der Dokumentation.

Falls Sie ein Neuankömmling bei ACL2 sind, ist es nicht empfehlenswert, dass sie durch volle Dokumentation durchwandern. Stattdessen fangen Sie bitte an mit dem  Touren und vielleicht  demos.

Wenn du immer noch Interesse an ACL2 hast, würden wir dir empfehlen eine Kopie von  Computer-Aided Reasoning: An Approach zu machen und es sorgfältig durchlesen. Mach Übungen mit  ACL2. Lerne "Die Methode".

Weniger effektiv als das Buchlesen und Übungenmachen, aber immer noch behilflich ist die ausgewählten Werke von Books and Papers about ACL2 and Its Applications zu lesen, lies das Dokumentationthema the-method, und Hyper-Card und dann setz deinen Weg fort durch Lehrbücher.

Dann empfehlen wir dir die ausgewählten Themen von "Major Topics" zu lesen.

  • EVENTS — top-level commands wie DEFUN und DEFTHM
  • PROGRAMMING — alle Common Lisp Functionen ACL2 supports
  • RULE-CLASSES — wie kann man ACL2's Benehmen mit regeln beeinflussen,
  • BOOKS — wie erschafft man re-usable databases von Regeln.

Die erfahrene Benutzer neigen oft dazu, das "Index" zu gebrauchen um die Konzepte anzuschauen, die sie in den Fehlermeldungen gesehen haben oder an denen sie sich schwach aus eigenen vergangenen ACL2-Erfahrungen erinnern.

Anmerkung: Wenn ACL2 auf dein Lokalsystem istalliert wurde, muss HTML Documentation lokal errreichbar sein. Man kann network durch Browsen deiner lokalen Kopie minimalisieren. Z.B. wenn ACL2 auf /usr/jones/acl2/vi-j installiert wurde, dann ist lokaler URL für diese Seite:
file:/usr/jones/acl2/vi-j/acl2-sources/doc/HTML/acl2-doc.html.
Viele ACL2 User machen eine browser Bookmark zu diesem File und nutzen ihre Browser, um täglich den Zugang zu der Dokumentation zu haben. Wenn du ACL2 erlangst, bitte fördere Users eine Lokalkopie der Dokumentation zu nutzen, anstatt Zugang durch das Web.

Anmerkung: Die Dokumentation ist verfügbar für Lesen im Web-browser (empfohlen), in der Emacs Info, mit Hilfe von ACL2: DOC Kommand, oder als ein gedrücktes Buch (etwa 1900 Seiten). Diese sind wie folgt verfügbar: doc/ subdirectory des adressnuches, über der ACL2 installiert ist. Wenn sie eine gedrückte Kopie lesen wollen, erhalten Sie eine Nachschriftversion hier (über 2 MB).


 

Lemma Bibliothek und Nutzen; Wie man beiträgt

Die Verteilung von ACL2 schließt einige Tools ein, die von Benutzer aufgebaut wurden. Die Mehrheit von denen sind ACL2 "books". Sie sind die Sammlungen von Definitionen und Theoreme, die nützlich für ihre Modelle und Beweise sein können. Fast alle verfügbare Bücher erscheinen mit Distribution, aber auch das Link oben führt zu zusätzliche Bücher der Unterstützung von ACL2 Werkstätten ("workshops") und nicht-standard Analyse ("nonstd").

Wir ermutigen stark die Benutzer zusätzliche Bücher vorzulegen bei Folgen die Anweisungen für Bücherbeitrage zu ACL2.

Wir verteilen auch einige Schnittstelletools, wie zum Beispiel Unterstützung für Einfügungsdrucken. Um diese zu erhalten, sehen Sie Utilities Sektion von  Bücher und Papiere über ACL2 und seine Applikationen. Manche Papiere aus dieser Sammlung enthalten Nutzen, Scripts, oder ACL2 Bücher des Problemgebiets in Fragen.


 

Wie man Bibliotheken und Dokumentation beiträgt

Wie bereits erwähnt, ermutigen wir stark die Benutzer zusätzliche Bücher vorzulegen bei Folgen die Anweisungen für Bücherbeitrage zu ACL2.

Wenn Sie auch einen Text geschrieben haben, der für andere ACL2 Benutzer hilfreich werden kann (oder so einen Text schreiben wollen), laden wir Ihnen ein, ihn zu unserer Gemeinschaft beizutragen. Diese Benutzerdokumentation kann in jeder Format sein, das von Web-Browser zu Lessen ist (zum Beispiel html, pdf, und einfachen Text). Benutzer-beigeträgt Dokumentation kann zurück linken zum ACL2 Eigendokumentation, mit Hilfe von folgendem Link: 

http://www.cs.utexas.edu/users/moore/acl2/current/MAKE-EVENT.html
(In Allgemeinen, ersetzen Sie die obere-Umschaltung des Dokumentationsthemas für "MAKE-EVENT" im Beispiel oben).

Um die Benutzerdokumentation beizutragen, senden Sie bitte ein E-mail zu den ACL2 Entwickler, zum Beispiel auf: acl2-bugs@utlists.utexas.edu.