NASALib est un effort de collaboration continu qui s'étend sur plus de trois décennies pour faciliter la recherche liée à la démonstration de théorèmes parrainée par la NASA (https://shemesh.larc.nasa.gov/fm/pvs/). Il consiste en une collection de développements formels (c'est-à-dire des bibliothèques ) écrits dans le système de vérification des prototypes (PVS), contribués par le SRI, la NASA, le NIA et la communauté PVS, et maintenus par l'équipe des méthodes formelles du LaRC.
La version actuelle de NASALib est la 7.1.2 (01/09/2023) et nécessite PVS 7.1.
Actuellement, NASALib se compose de 62 bibliothèques de niveau supérieur , contenant au total environ 38 000 formules éprouvées.
| Bibliothèque | Description |
|---|---|
| Accord | Cadre d’analyse des algorithmes de détection et de résolution des conflits aériens |
| affine_arith | Formalisation de l'arithmétique affine et stratégie d'évaluation de fonctions polynomiales avec des variables sur des domaines d'intervalles |
| algèbre | Groupes, monoïdes, anneaux, etc. |
| analyse | Analyse réelle, limites, continuité, dérivées, intégrales |
| ASPIC | Sémantique dénotationnelle de la programmation d'ensembles de réponses |
| aviation | Définitions et propriétés de prise en charge pour les formalisations liées à l'aviation |
| Bernstein | Formalisation des polynômes de Bernstein multivariés |
| GCC | Formalisation de divers critères de rupture |
| complexe | Nombres complexes |
| complexe_alt | Formalisation alternative des nombres complexes |
| intégration_complexe | Intégration complexe |
| co_structures | Séquences de longueur dénombrable définies comme types de données co-algébriques |
| digrammes | Graphes orientés : circuits, sous-arbres maximaux, chemins, DAG |
| dL | Logique dynamique différentielle |
| exact_real_arith | Arithmétique réelle exacte, y compris les fonctions trigonométriques |
| exemples | Exemples d'application des fonctionnalités fournies par NASALib |
| extend_nnreal | Réels non négatifs étendus |
| fast_environ | Approximations des fonctions numériques standards |
| tolérance_de_défaut | Protocoles de tolérance aux pannes |
| flotter | Arithmétique à virgule flottante |
| graphiques | Théorie des graphes |
| intervalle_arith | Arithmétique d'intervalle et approximations numériques. Comprend des stratégies numériques automatisées pour calculer des approximations numériques et des intervalles pour vérifier la satisfiabilité et la validité de formules à valeur réelle simplement quantifiées. Ce développement inclut une formalisation de la logique temporelle de l'intervalle Allen |
| entiers | Division entière, pgcd, mod, factorisation première, min, max |
| lebesgue | Intégrale de Lebesgue avec connexion à Intégrale de Riemann |
| algèbre_linéaire | Algèbre linéaire |
| segments_lignes | Segments de ligne bidimensionnels |
| lnexp | Fonctions logarithmiques, exponentielles et hyperboliques. & Définitions fondamentales des fonctions logarithmiques, exponentielles et hyperboliques |
| LTL | Logique temporelle linéaire |
| matrices | Spécification exécutable des matrices MxN. Cette bibliothèque comprend le calcul d'opérations matricielles inverses et de base telles que l'addition et la multiplication |
| mesure_intégration | Algèbres sigma, mesures, lemmes de Fubini-Tonelli |
| MetiTarski | Intégration de MetiTarski, un prouveur automatisé de théorèmes pour les fonctions à valeurs réelles |
| espace_métrique | Domaines avec une métrique de distance, continuité et continuité uniforme |
| mv_analyse | Analyse réelle multivariée : normes, limites, continuité, dérivées, optimisation, etc. |
| mult_poly | Polynômes multivariés et ensembles semi-algébriques. |
| nominal | Raisonnement équationnel nominal |
| Nombres | Théorie élémentaire des nombres |
| ODE | Équations différentielles ordinaires |
| ordres | Ordres abstraits, treillis, points fixes |
| polygones | Polygones bidimensionnels |
| polygon_merge | Fusion de polygones bidimensionnels sans générer de trous |
| pouvoir | Fonction de puissance généralisée (sans ln/exp) |
| probabilité | Théorie des probabilités |
| PVS0 | Formalisation des concepts fondamentaux de calculabilité |
| pvsio_utils | Ajouts à PVSio, une bibliothèque standard PVS pour l'animation des spécifications PVS |
| réels | Sommations, sup, inf, sqrt sur les réels, valeur absolue, etc. |
| Riemann | intégrale de Riemann |
| scott | Topologie Scott |
| série | Séries entières, test de comparaison, test de ratio, théorème de Taylor |
| sets_aux | Ensembles de puissance, ordres, cardinalité sur des ensembles infinis. Comprend des faits fonctionnels et relationnels basés sur l'axiome du choix et des relations de raffinement basées sur des relations d'équivalence. |
| formes | Formes 2D : triangle, parallélogramme, rectangle, segment circulaire |
| sigma_set | Sommes sur des ensembles infinis et dénombrables |
| tri | Algorithmes de tri |
| constructions | Tableaux bornés, séquences finies, sacs et plusieurs autres structures |
| Tempête | Formalisation du théorème de Sturm pour les polynômes univariés. Inclut les stratégies sturm et mono-poly pour prouver automatiquement les relations polynomiales univariées sur un intervalle réel |
| Tarski | Formalisation du théorème de Tarski pour les polynômes univariés. Comprend la stratégie tarski pour prouver automatiquement les systèmes de relations polynomiales univariées sur la ligne réelle |
| topologie | Continuité, homéomorphismes, espaces connectés et compacts, ensembles/fonctions de Borel |
| trigonométrie | Trigonométrie : définitions, identités, approximations |
| TRS | Systèmes de réécriture de termes et algorithme d'unification Robinson |
| TU_jeux | Jeux TU coopératifs |
| vect_analyse | Limites, continuité et dérivées des fonctions vectorielles |
| vecteurs | Vecteurs 2D, 3D, 4D et n dimensions |
| alors que | Sémantique du langage de programmation While |
NASALib fournit également une collection de scripts qui automatisent plusieurs tâches.
proveit (*) - Exécute PVS en mode batchprovethem (*) - Exécute proveit sur plusieurs bibliothèquespvsio (*) - Utilitaire de ligne de commande pour exécuter l'évaluateur au sol PVSio.prove-all - Exécute proveit sur chaque bibliothèque de NASALib en encapsulant provethem afin de fournir un type d'exécution spécifique.cleanbin-all - Nettoie les fichiers .pvscontext et binaires des bibliothèques PVS.find-all - Recherche les chaînes correspondant à une expression régulière donnée dans les bibliothèques PVS.dependencygraph - Génère un graphique de dépendances de bibliothèque pour les bibliothèques du répertoire actuel.dependency-all - Génère les graphiques de dépendances pour les bibliothèques PVS dans le dossier actuel.Cliquez ici pour plus de détails sur ces scripts.
(*) Déjà inclus dans la distribution PVS 7.1.
NASALib (v7.0.1) est entièrement compatible avec VSCode-PVS, une interface graphique moderne pour PVS basée sur Visual Studio Code. La dernière version de NASALib peut être installée à partir de VSCode-PVS.
Pour les utilisateurs avancés de PVS, la version de développement est disponible sur GitHub. Pour cloner la version de développement, tapez la commande suivante dans le répertoire où PVS 7.0 est installé. Désormais, ce répertoire sera appelé
$ git clone http://github.com/nasa/pvslib nasalib La commande ci-dessus placera une copie de la bibliothèque dans le répertoire
Les groups de bibliothèques sont désormais obsolètes . La bibliothèque group a été intégrée à algebra . Un lien symbolique est toujours fourni pour des raisons de compatibilité ascendante, mais son utilisation est déconseillée. Chaque mention de groups doit être remplacée par algebra .
La bibliothèque trig_fnd est désormais obsolète . Il est toujours prévu pour une compatibilité ascendante, mais il devrait être remplacé par trig . La nouvelle bibliothèque trig , qui était autrefois un axiomatique, est désormais fondamentale. Cependant, contrairement à trig_fnd , les définitions trigonométriques sont basées sur des séries infinies plutôt que sur des intégrales. Ce changement réduit considérablement la vérification de type des théories impliquant des fonctions trigonométriques. Le passage de trig_fnd à trig ne devrait pas avoir d'impact majeur dans vos développements formels puisque les noms des définitions et des lemmes sont les mêmes. Cependant, l’importation de la théorie peut être légèrement différente.
Les développements PVS TCASII , WellClear et DAIDALUS sont désormais disponibles dans le cadre de la distribution GitHub WellClear. Le développement PVS PRECiSA est désormais disponible dans le cadre de la distribution GitHub PRECiSA. Le développement PVS PolyCARP est désormais disponible dans le cadre de la distribution GitHub PolyCARP.
Les instructions suivantes supposent que NASALib se trouve dans le répertoire
PVS_LIBRARY_PATH Si elle n'existe pas, crée une telle variable et avec le chemin de ce répertoire comme seul contenu. Il est généralement très utile que vos systèmes shell créent cette variable au démarrage. À cette fin, et en fonction de votre shell, vous souhaiterez peut-être ajouter l'une des lignes suivantes dans votre script de démarrage. Pour le shell C (csh ou tcsh), vous pouvez ajouter cette ligne dans ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " Pour le shell Borne (bash ou sh), ajoutez cette ligne dans ~/.bashrc ou ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " Si vous avez déjà installé NASALib, supprimez le fichier ~/.pvs.lisp ou, si vous avez une configuration spéciale dans ce fichier, supprimez la ligne suivante
( load " /nasalib/pvs-patches.lisp " ) Enfin, allez dans le répertoire
La commande install-scripts mettra à jour et installera les scripts NASALib selon les besoins.
$ ./install-scriptsLes anciennes versions de NASALib sont disponibles sur http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
NASALib s'est développé au fil des années grâce à la contribution de plusieurs personnes, parmi lesquelles :
Si nous avons attribué à tort un développement PVS ou si vous avez contribué à NASALib et que votre nom n'est pas inclus ici, veuillez nous le faire savoir.
Si vous souhaitez contribuer, veuillez lire ce guide.
NASALib est un ensemble de spécifications formelles dont la plupart sont dans le domaine public depuis plusieurs années. L'équipe des méthodes formelles de la NASA LaRC maintient toujours ces développements. Pour les développements initialement réalisés par l'équipe Méthodes Formelles, ces développements sont considérés comme de la recherche fondamentale qui ne constitue pas un logiciel. Les contributions apportées par d'autres peuvent avoir des licences particulières, qui sont répertoriées dans le fichier top.pvs de chaque répertoire respectif. En cas de doute, veuillez contacter les développeurs de chaque contribution, qui sont également répertoriés dans ce fichier.
Les correctifs PVS, qui sont inclus dans le répertoire pvs-patches , font partie du code source PVS et sont couverts par la licence open source PVS.
Certaines stratégies de preuve nécessitent des outils de recherche tiers, par exemple MetiTarski et Z3. Pour plus de commodité, ils sont inclus dans ce référentiel avec la permission de leurs auteurs. Les licences pour ces outils sont également incluses, le cas échéant.
Profitez-en.
L’équipe Méthodes Formelles du LaRC
César Muñoz Mariano Moscato
