NASALib es un esfuerzo de colaboración continuo que se ha extendido por más de 3 décadas para ayudar en la investigación relacionada con la demostración de teoremas patrocinado por la NASA (https://shemesh.larc.nasa.gov/fm/pvs/). Consiste en una colección de desarrollo formal (es decir, bibliotecas ) escrito en el Sistema de Verificación de Prototipos (PVS), aportado por SRI, NASA, NIA y la comunidad PVS, y mantenido por el Equipo de Métodos Formales de LaRC.
La versión actual de NASALib es 7.1.2 (01/09/2023) y requiere PVS 7.1.
Actualmente, NASALib consta de 62 bibliotecas de alto nivel , que contienen alrededor de 38.000 fórmulas probadas en total.
| Biblioteca | Descripción |
|---|---|
| Acuerdo | Marco para el análisis de algoritmos de detección y resolución de conflictos de tráfico aéreo |
| affine_arith | Formalización de la aritmética afín y estrategia para evaluar funciones polinómicas con variables en dominios de intervalo. |
| álgebra | Grupos, monoides, anillos, etc. |
| análisis | Análisis real, límites, continuidad, derivadas, integrales. |
| ÁSPID | Semántica denotacional de la programación de conjuntos de respuestas |
| aviación | Definiciones y propiedades de soporte para formalizaciones relacionadas con la aviación |
| bernstein | Formalización de polinomios multivariados de Bernstein. |
| CCG | Formalización de diversos criterios de rescisión |
| complejo | Números complejos |
| complejo_alt | Formalización alternativa de números complejos. |
| integración_compleja | Integración compleja |
| co_estructuras | Secuencias de longitud contable definidas como tipos de datos coalgebraicos |
| dígrafos | Gráficos dirigidos: circuitos, subárboles máximos, caminos, DAG |
| dL | Lógica dinámica diferencial |
| exacta_real_arith | Aritmética real exacta incluyendo funciones trigonométricas |
| ejemplos | Ejemplos de aplicación de la funcionalidad proporcionada por NASALib |
| extendido_nnreal | Reales extendidos no negativos |
| rápido_aprox. | Aproximaciones de funciones numéricas estándar |
| tolerancia_fallas | Protocolos de tolerancia a fallos |
| flotar | Aritmética de coma flotante |
| graficos | Teoría de grafos |
| intervalo_arith | Aritmética de intervalos y aproximaciones numéricas. Incluye estrategias numéricas automatizadas para calcular aproximaciones numéricas e intervalos para comprobar la satisfacibilidad y validez de fórmulas de valores reales cuantificadas de forma sencilla. Este desarrollo incluye una formalización de la lógica temporal del intervalo de Allen. |
| enteros | División de enteros, mcd, mod, factorización prima, mínimo, máximo |
| lebesgue | Integral de Lebesgue con conexión a Integral de Riemann |
| álgebra_lineal | Álgebra lineal |
| segmentos_de_linea | segmentos de línea bidimensionales |
| lnexp | Funciones logarítmicas, exponenciales e hiperbólicas. & Definiciones fundamentales de funciones logaritmicas, exponenciales e hiperbólicas |
| LTL | Lógica temporal lineal |
| matrices | Especificación ejecutable de matrices MxN. Esta biblioteca incluye cálculo de operaciones matriciales básicas e inversas, como suma y multiplicación. |
| medida_integración | Álgebras de sigma, medidas, lemas de Fubini-Tonelli |
| MetiTarski | Integración de MetiTarski, un demostrador de teoremas automatizado para funciones de valor real |
| espacio_métrico | Dominios con métrica de distancia, continuidad y continuidad uniforme. |
| análisis_mv | Análisis real multivariante: normas, límites, continuidad, derivadas, optimización, etc. |
| multi_poli | Polinomios multivariados y conjuntos semialgebriicos. |
| nominal | Razonamiento ecuacional nominal |
| números | Teoría de números elemental |
| EDO | Ecuaciones diferenciales ordinarias |
| pedidos | Órdenes abstractas, celosías, puntos fijos. |
| polígonos | polígonos bidimensionales |
| fusión_polígono | Fusión de polígonos bidimensionales sin generar agujeros. |
| fuerza | Función de potencia generalizada (sin ln/exp) |
| probabilidad | Teoría de la probabilidad |
| PVS0 | Formalización de conceptos fundamentales de computabilidad. |
| pvsio_utils | Adiciones a PVSio, una biblioteca estándar de PVS para animación de especificaciones de PVS |
| reales | Sumas, sup, inf, sqrt sobre reales, valor absoluto, etc. |
| Riemann | integral de riemann |
| escocés | topología de Scott |
| serie | Series de potencias, prueba de comparación, prueba de razón, teorema de Taylor |
| conjuntos_aux | Conjuntos de potencias, órdenes, cardinalidad sobre conjuntos infinitos. Incluye hechos funcionales y relacionales basados en el axioma de elección y relaciones de refinamiento basadas en relaciones de equivalencia. |
| formas | Formas 2D: triángulo, paralelogramo, rectángulo, segmento circular |
| conjunto_sigma | Sumas de conjuntos contablemente infinitos |
| clasificación | Algoritmos de clasificación |
| estructuras | Matrices acotadas, secuencias finitas, bolsas y varias otras estructuras. |
| Sturm | Formalización del teorema de Sturm para polinomios univariados. Incluye estrategias sturm y mono-poly para demostrar automáticamente relaciones polinómicas univariadas en un intervalo real. |
| Tarski | Formalización del teorema de Tarski para polinomios univariados. Incluye la estrategia tarski para probar automáticamente sistemas de relaciones polinómicas univariadas en la recta real. |
| topología | Continuidad, homeomorfismos, espacios conectados y compactos, conjuntos/funciones de Borel |
| trigonometría | Trigonometría: definiciones, identidades, aproximaciones. |
| TRS | Sistemas de reescritura de términos y algoritmo de unificación de Robinson. |
| TU_juegos | Juegos cooperativos TU |
| análisis_vect | Límites, continuidad y derivadas de funciones vectoriales. |
| vectores | Vectores 2-D, 3-D, 4-D y n-dimensionales |
| mientras | Semántica del lenguaje de programación Mientras |
NASALib también proporciona una colección de scripts que automatizan varias tareas.
proveit (*) - Ejecuta PVS en modo por lotesprovethem (*) - Ejecuta proveit en varias bibliotecaspvsio (*): utilidad de línea de comandos para ejecutar el evaluador de terreno PVSio.prove-all : ejecuta proveit en cada biblioteca de NASALib envolviendo provethem para proporcionar un tipo de ejecución específico.cleanbin-all : limpia archivos .pvscontext y binarios de las bibliotecas PVS.find-all : busca cadenas que coincidan con expresiones regulares determinadas en bibliotecas PVS.dependencygraph : genera un gráfico de dependencia de bibliotecas para las bibliotecas en el directorio actual.dependency-all : genera los gráficos de dependencia para las bibliotecas PVS en la carpeta actual.Haga clic aquí para obtener más detalles sobre estos scripts.
(*) Ya incluido en la distribución PVS 7.1.
NASALib (v7.0.1) es totalmente compatible con VSCode-PVS, una interfaz gráfica moderna para PVS basada en Visual Studio Code. La última versión de NASALib se puede instalar desde VSCode-PVS.
Para usuarios avanzados de PVS, la versión de desarrollo está disponible en GitHub. Para clonar la versión de desarrollo, escriba el siguiente comando dentro del directorio donde está instalado PVS 7.0. De ahora en adelante, nos referiremos a ese directorio como
$ git clone http://github.com/nasa/pvslib nasalib El comando anterior colocará una copia de la biblioteca en el directorio
Los groups de bibliotecas ahora están en desuso . La biblioteca group se integró al algebra . Todavía se proporciona un enlace simbólico para compatibilidad con versiones anteriores, pero se desaconseja su uso. Cada mención a groups debería ser reemplazada por algebra .
La biblioteca trig_fnd ahora está en desuso . Todavía se proporciona por compatibilidad con versiones anteriores, pero debe reemplazarse por trig . La nueva biblioteca trig , que solía ser axiomática, ahora es fundamental. Sin embargo, a diferencia de trig_fnd , las definiciones trigonométricas se basan en series infinitas, en lugar de integrales. Este cambio reduce considerablemente la verificación de tipos de teorías que involucran funciones trigonométricas. El cambio de trig_fnd a trig no debería tener un impacto importante en sus desarrollos formales ya que los nombres de las definiciones y los lemas son los mismos. Sin embargo, la importación de teorías puede ser ligeramente diferente.
Los desarrollos PVS TCASII , WellClear y DAIDALUS ahora están disponibles como parte de la distribución GitHub WellClear. El desarrollo PVS PRECiSA ya está disponible como parte de la distribución GitHub PRECiSA. El desarrollo PVS PolyCARP ahora está disponible como parte de la distribución GitHub PolyCARP.
Las siguientes instrucciones asumen que NASALib está ubicado en el directorio
PVS_LIBRARY_PATH Si no existe, crea dicha variable y con la ruta de este directorio como único contenido. Generalmente es muy útil que sus sistemas shell creen esta variable al inicio. Con este fin, y dependiendo de su shell, es posible que desee agregar una de las siguientes líneas en su secuencia de comandos de inicio. Para C shell (csh o tcsh), puede agregar esta línea en ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " Para Borne Shell (bash o sh), agregue esta línea en ~/.bashrc o ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " Si tuvo una instalación anterior de NASALib, elimine el archivo ~/.pvs.lisp o, si tiene una configuración especial en ese archivo, elimine la siguiente línea
( load " /nasalib/pvs-patches.lisp " ) Finalmente, vaya al directorio
El comando install-scripts actualizará e instalará los scripts de NASALib según sea necesario.
$ ./install-scriptsLas versiones anteriores de NASALib están disponibles en http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
NASALib ha crecido a lo largo de los años gracias al aporte de varias personas, entre ellas:
Si hemos atribuido incorrectamente un desarrollo de PVS o usted ha contribuido a NASALib y su nombre no está incluido aquí, háganoslo saber.
Si desea contribuir, lea esta guía.
NASALib es una colección de especificaciones formales, la mayoría de las cuales han sido de dominio público durante varios años. El Equipo de Métodos Formales de NASA LaRC aún mantiene estos desarrollos. Para los desarrollos realizados originalmente por el Equipo de Métodos Formales, estos desarrollos se consideran investigaciones fundamentales que no constituyen software. Las contribuciones realizadas por otros pueden tener licencias particulares, que se enumeran en el archivo top.pvs en cada directorio respectivo. En caso de duda, póngase en contacto con los desarrolladores de cada contribución, que también figuran en ese archivo.
Los parches PVS, que se incluyen en el directorio pvs-patches , forman parte del código fuente de PVS y están cubiertos por la licencia de código abierto de PVS.
Algunas estrategias de prueba requieren herramientas de investigación de terceros, por ejemplo, MetiTarski y Z3. Para mayor comodidad, se incluyen en este repositorio con el permiso de sus autores. También se incluyen licencias para estas herramientas según corresponda.
Disfrútala.
El equipo de métodos formales en LaRC
César Muñoz Mariano Moscato
