NASALib ist eine kontinuierliche, über drei Jahrzehnte andauernde Gemeinschaftsinitiative zur Unterstützung der von der NASA gesponserten Forschung im Zusammenhang mit Theorembeweisen (https://shemesh.larc.nasa.gov/fm/pvs/). Es besteht aus einer Sammlung formaler Entwicklungen (d. h. Bibliotheken ), die im Prototype Verification System (PVS) geschrieben, von SRI, NASA, NIA und der PVS-Community beigesteuert und vom Team für formale Methoden bei LaRC gepflegt werden.
Die aktuelle Version von NASALib ist 7.1.2 (01.09.2023) und erfordert PVS 7.1.
Derzeit besteht NASALib aus 62 Top-Level -Bibliotheken, die insgesamt etwa 38.000 bewährte Formeln enthalten.
| Bibliothek | Beschreibung |
|---|---|
| Übereinstimmung | Framework für die Analyse von Algorithmen zur Erkennung und Lösung von Flugverkehrskonflikten |
| affine_arith | Formalisierung der affinen Arithmetik und Strategie zur Auswertung von Polynomfunktionen mit Variablen auf Intervalldomänen |
| Algebra | Gruppen, Monoide, Ringe usw |
| Analyse | Reale Analysis, Grenzen, Kontinuität, Ableitungen, Integrale |
| ASP | Denotationssemantik der Antwortsatzprogrammierung |
| Luftfahrt | Unterstützen Sie Definitionen und Eigenschaften für luftfahrtbezogene Formalisierungen |
| Bernstein | Formalisierung multivariater Bernstein-Polynome |
| CCG | Formalisierung diverser Abbruchkriterien |
| Komplex | Komplexe Zahlen |
| complex_alt | Alternative Formalisierung komplexer Zahlen |
| komplexe_integration | Komplexe Integration |
| co_structures | Folgen abzählbarer Länge, definiert als co-algebraische Datentypen |
| Digraphen | Gerichtete Graphen: Schaltkreise, maximale Teilbäume, Pfade, DAGs |
| dL | Differenzielle dynamische Logik |
| exakter_realer_arith | Exakte echte Arithmetik einschließlich trigonometrischer Funktionen |
| Beispiele | Anwendungsbeispiele der von NASALib bereitgestellten Funktionalität |
| erweitert_nnreal | Erweiterte nichtnegative Realzahlen |
| schnell_ca | Approximationen standardmäßiger numerischer Funktionen |
| Fehlertoleranz | Fehlertoleranzprotokolle |
| schweben | Gleitkomma-Arithmetik |
| Grafiken | Graphentheorie |
| Intervall_arith | Intervallarithmetik und numerische Näherungen. Enthält automatisierte numerische Strategien zur Berechnung numerischer Näherungen und Intervalle zur Überprüfung der Erfüllbarkeit und Gültigkeit einfach quantifizierter Formeln mit reellen Werten. Diese Entwicklung beinhaltet eine Formalisierung der Allen-Intervall-Zeitlogik |
| ints | Ganzzahldivision, gcd, mod, Primfaktorzerlegung, min, max |
| lebesgue | Lebesgue-Integral mit Verbindung zum Riemann-Integral |
| lineare_Algebra | Lineare Algebra |
| line_segments | 2-dimensionale Liniensegmente |
| lnexp | Logarithmus, Exponential- und Hyperbolikfunktionen. & Grundlegende Definitionen von Logarithmus-, Exponential- und Hyperbelfunktionen |
| LTL | Lineare zeitliche Logik |
| Matrizen | Ausführbare Spezifikation von MxN-Matrizen. Diese Bibliothek umfasst die Berechnung inverser und grundlegender Matrixoperationen wie Addition und Multiplikation |
| Measure_Integration | Sigma-Algebren, Maße, Fubini-Tonelli-Lemmas |
| MetiTarski | Integration von MetiTarski, einem automatisierten Theorembeweis für reellwertige Funktionen |
| metric_space | Domänen mit Distanzmetrik, Kontinuität und einheitlicher Kontinuität |
| mv_analysis | Multivariate reelle Analyse: Normen, Grenzwerte, Kontinuität, Ableitungen, Optimierung usw. |
| mult_poly | Multivariate Polynome und semialgebrische Mengen. |
| nominal | Nominales Gleichungsdenken |
| Zahlen | Elementare Zahlentheorie |
| ODEs | Gewöhnliche Differentialgleichungen |
| Bestellungen | Abstrakte Ordnungen, Gitter, Fixpunkte |
| Polygone | 2-dimensionale Polygone |
| polygon_merge | Zusammenführung zweidimensionaler Polygone ohne Löcher zu erzeugen |
| Leistung | Verallgemeinerte Potenzfunktion (ohne ln/exp) |
| Wahrscheinlichkeit | Wahrscheinlichkeitstheorie |
| PVS0 | Formalisierung grundlegender Berechenbarkeitskonzepte |
| pvsio_utils | Ergänzungen zu PVSio, einer PVS-Standardbibliothek zur Animation von PVS-Spezifikationen |
| Reals | Summationen, sup, inf, sqrt über die reellen Zahlen, Absolutwerte usw |
| Riemann | Riemann-Integral |
| Scott | Scott-Topologie |
| Serie | Potenzreihen, Vergleichstest, Verhältnistest, Satz von Taylor |
| setzt_aux | Potenzmengen, Ordnungen, Kardinalität über unendliche Mengen. Enthält funktionale und relationale Fakten basierend auf dem Axiom of Choice und Verfeinerungsrelationen basierend auf Äquivalenzrelationen |
| Formen | 2D-Formen: Dreieck, Parallelogramm, Rechteck, Kreissegment |
| sigma_set | Summationen über abzählbar unendliche Mengen |
| Sortierung | Sortieralgorithmen |
| Strukturen | Begrenzte Arrays, endliche Sequenzen, Taschen und verschiedene andere Strukturen |
| Sturm | Formalisierung des Sturm-Theorems für univariate Polynome. Enthält die Strategien sturm und mono-poly zum automatischen Beweis univariater Polynombeziehungen über ein reales Intervall |
| Tarski | Formalisierung des Satzes von Tarski für univariate Polynome. Beinhaltet Strategietarski zum automatischen Beweisen von Systemen univariater Polynombeziehungen auf der reellen Linie |
| Topologie | Kontinuität, Homöomorphismen, zusammenhängende und kompakte Räume, Borel-Mengen/-Funktionen |
| trig | Trigonometrie: Definitionen, Identitäten, Näherungen |
| TRS | Term-Rewrite-Systeme und Robinson-Vereinigungsalgorithmus |
| TU_Spiele | Kooperative TU-Spiele |
| vect_analysis | Grenzen, Stetigkeit und Ableitungen von Vektorfunktionen |
| Vektoren | 2D-, 3D-, 4D- und n-dimensionale Vektoren |
| während | Semantik für die Programmiersprache While |
NASALib bietet außerdem eine Sammlung von Skripten, die mehrere Aufgaben automatisieren.
proveit (*) – Führt PVS im Batch-Modus ausprovethem (*) – Führt proveit in mehreren Bibliotheken auspvsio (*) – Befehlszeilen-Dienstprogramm zum Ausführen des PVSio-Bodenauswerters.prove-all – Führt proveit für jede Bibliothek in NASALib aus, indem provethem eingeschlossen wird, um eine bestimmte Art von Ausführung bereitzustellen.cleanbin-all – Bereinigt .pvscontext und Binärdateien aus PVS-Bibliotheken.find-all – Sucht nach Zeichenfolgen, die mit einem bestimmten regulären Ausdruck in PVS-Bibliotheken übereinstimmen.dependencygraph – Erstellt ein Bibliotheksabhängigkeitsdiagramm für Bibliotheken im aktuellen Verzeichnis.dependency-all – Erzeugt die Abhängigkeitsdiagramme für die PVS-Bibliotheken im aktuellen Ordner.Klicken Sie hier für weitere Details zu diesen Skripten.
(*) Bereits in der PVS 7.1-Distribution enthalten.
NASALib (v7.0.1) ist vollständig kompatibel mit VSCode-PVS, einer modernen grafischen Schnittstelle zu PVS basierend auf Visual Studio Code. Die neueste Version von NASALib kann über VSCode-PVS installiert werden.
Für fortgeschrittene PVS-Benutzer ist die Entwicklungsversion auf GitHub verfügbar. Um die Entwicklungsversion zu klonen, geben Sie den folgenden Befehl in das Verzeichnis ein, in dem PVS 7.0 installiert ist. Von nun an wird dieses Verzeichnis als
$ git clone http://github.com/nasa/pvslib nasalib Der obige Befehl legt eine Kopie der Bibliothek im Verzeichnis
Die groups sind jetzt veraltet . Die group wurde in algebra integriert. Aus Gründen der Abwärtskompatibilität wird weiterhin ein symbolischer Link bereitgestellt, von dessen Verwendung jedoch abgeraten wird. Jede Erwähnung von groups sollte durch algebra ersetzt werden.
Die Bibliothek trig_fnd ist jetzt veraltet . Es wird weiterhin aus Gründen der Abwärtskompatibilität bereitgestellt, sollte jedoch durch trig ersetzt werden. Die neue Bibliothek trig , die früher eine Selbstverständlichkeit war, ist jetzt grundlegend. Im Gegensatz zu trig_fnd basieren trigonometrische Definitionen jedoch auf unendlichen Reihen und nicht auf Integralen. Diese Änderung reduziert die Typprüfung von Theorien mit trigonometrischen Funktionen erheblich. Der Wechsel von trig_fnd zu trig sollte keine großen Auswirkungen auf Ihre formalen Entwicklungen haben, da die Namen von Definitionen und Lemmata gleich sind. Der Theorieimport kann jedoch etwas anders sein.
Die PVS-Entwicklungen TCASII , WellClear und DAIDALUS sind jetzt als Teil der GitHub WellClear-Distribution verfügbar. Die PVS-Entwicklung PRECiSA ist jetzt als Teil der GitHub PRECiSA-Distribution verfügbar. Die PVS-Entwicklung PolyCARP ist jetzt als Teil der GitHub PolyCARP-Distribution verfügbar.
Bei den folgenden Anweisungen wird davon ausgegangen, dass sich NASALib im Verzeichnis
PVS_LIBRARY_PATH hinzu Wenn sie nicht vorhanden ist, wird eine solche Variable erstellt, wobei der Pfad dieses Verzeichnisses nur der Inhalt ist. Normalerweise ist es sehr nützlich, wenn Ihre Shell-Systeme diese Variable beim Start erstellen. Zu diesem Zweck und abhängig von Ihrer Shell möchten Sie möglicherweise eine der folgenden Zeilen in Ihr Startskript einfügen. Für die C-Shell (csh oder tcsh) können Sie diese Zeile in ~/.cshrc hinzufügen:
setenv PVS_LIBRARY_PATH " /nasalib " Fügen Sie für die Borne-Shell (bash oder sh) diese Zeile entweder in ~/.bashrc oder ~/.profile hinzu:
export PVS_LIBRARY_PATH= " /nasalib " Wenn Sie eine frühere Installation von NASALib hatten, entfernen Sie entweder die Datei ~/.pvs.lisp oder, wenn Sie eine spezielle Konfiguration in dieser Datei haben, entfernen Sie die folgende Zeile
( load " /nasalib/pvs-patches.lisp " ) Gehen Sie abschließend in das Verzeichnis
Der Befehl install-scripts aktualisiert und installiert NASALib-Skripte nach Bedarf.
$ ./install-scriptsÄltere Versionen von NASALib sind unter http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library verfügbar.
NASALib ist im Laufe der Jahre dank des Beitrags mehrerer Personen gewachsen, darunter:
Wenn wir eine PVS-Entwicklung fälschlicherweise zugeordnet haben oder Sie zu NASALib beigetragen haben und Ihr Name hier nicht aufgeführt ist, teilen Sie uns dies bitte mit.
Wenn Sie einen Beitrag leisten möchten, lesen Sie bitte diesen Leitfaden.
NASALib ist eine Sammlung formaler Spezifikationen, von denen die meisten seit mehreren Jahren öffentlich zugänglich sind. Das Team für formale Methoden am NASA LaRC pflegt diese Entwicklungen weiterhin. Bei den ursprünglich vom Formal Methods Team durchgeführten Entwicklungen handelt es sich um Grundlagenforschung, die keine Software darstellt. Für Beiträge Dritter gelten ggf. besondere Lizenzen, die in der Datei top.pvs im jeweiligen Verzeichnis aufgeführt sind. Im Zweifelsfall wenden Sie sich bitte an die Entwickler des jeweiligen Beitrags, die ebenfalls in der Datei aufgeführt sind.
PVS-Patches, die im Verzeichnis pvs-patches enthalten sind, sind Teil des PVS-Quellcodes und unterliegen der PVS-Open-Source-Lizenz.
Einige Beweisstrategien erfordern Recherchetools von Drittanbietern, z. B. MetiTarski und Z3. Der Einfachheit halber werden sie mit Genehmigung ihrer Autoren in dieses Repository aufgenommen. Gegebenenfalls sind auch Lizenzen für diese Tools enthalten.
Genießen Sie es.
Das Team für formale Methoden bei LaRC
César Muñoz Mariano Moscato
