NASALib é um esforço colaborativo contínuo que já dura mais de 3 décadas, para auxiliar na pesquisa relacionada à prova de teoremas patrocinada pela NASA (https://shemesh.larc.nasa.gov/fm/pvs/). Consiste em uma coleção de desenvolvimento formal (ou seja, bibliotecas ) escrito no Prototype Verification System (PVS), contribuído pelo SRI, NASA, NIA e a comunidade PVS, e mantido pela Equipe de Métodos Formais do LaRC.
A versão atual do NASALib é 7.1.2 (2023/09/01) e requer PVS 7.1.
Atualmente, NASALib consiste em 62 bibliotecas de nível superior , contendo cerca de 38 mil fórmulas comprovadas no total.
| Biblioteca | Descrição |
|---|---|
| Acordo | Estrutura para análise de algoritmos de detecção e resolução de conflitos de tráfego aéreo |
| affine_arith | Formalização de aritmética afim e estratégia para avaliação de funções polinomiais com variáveis em domínios intervalares |
| álgebra | Grupos, monóides, anéis, etc. |
| análise | Análise real, limites, continuidade, derivadas, integrais |
| ASP | Semântica denotacional de programação de conjunto de respostas |
| aviação | Definições e propriedades de suporte para formalizações relacionadas à aviação |
| Bernstein | Formalização de polinômios multivariados de Bernstein |
| CCG | Formalização de diversos critérios de rescisão |
| complexo | Números complexos |
| complexo_alt | Formalização alternativa de números complexos |
| integração_complexa | Integração complexa |
| co_estruturas | Sequências de comprimento contável definidas como tipos de dados co-algébricos |
| dígrafos | Gráficos direcionados: circuitos, subárvores máximas, caminhos, DAGs |
| dL | Lógica Dinâmica Diferencial |
| exact_real_arith | Aritmética real exata, incluindo funções trigonométricas |
| exemplos | Exemplos de aplicação da funcionalidade disponibilizada pelo NASALib |
| estendido_nnreal | Reais não negativos estendidos |
| rápido_aproximadamente | Aproximações de funções numéricas padrão |
| tolerância_a falhas | Protocolos de tolerância a falhas |
| flutuador | Aritmética de ponto flutuante |
| gráficos | Teoria dos grafos |
| intervalo_arith | Aproximações aritméticas e numéricas de intervalo. Inclui estratégias numéricas automatizadas para calcular aproximações numéricas e intervalos para verificar a satisfatibilidade e validade de fórmulas de valor real simplesmente quantificadas. Este desenvolvimento inclui uma formalização da lógica temporal do intervalo de Allen |
| entradas | Divisão inteira, mdc, mod, fatoração primária, mínimo, máximo |
| lebesgue | Integral de Lebesgue com conexão com Integral de Riemann |
| álgebra_linear | Álgebra linear |
| segmentos_linha | Segmentos de linha bidimensionais |
| lnexp | Funções logarítmicas, exponenciais e hiperbólicas. & Definições básicas de funções logarítmicas, exponenciais e hiperbólicas |
| LTL | Lógica Temporal Linear |
| matrizes | Especificação executável de matrizes MxN. Esta biblioteca inclui cálculo de operações matriciais inversas e básicas, como adição e multiplicação |
| medida_integração | Álgebras Sigma, medidas, Lemas de Fubini-Tonelli |
| MetiTarski | Integração do MetiTarski, um provador automatizado de teoremas para funções com valor real |
| espaço_métrico | Domínios com métrica de distância, continuidade e continuidade uniforme |
| mv_análise | Análise real multivariada: normas, limites, continuidade, derivadas, otimização, etc. |
| mult_poly | Polinômios multivariados e conjuntos semialgébricos. |
| nominal | Raciocínio equacional nominal |
| números | Teoria elementar dos números |
| EDOs | Equações Diferenciais Ordinárias |
| pedidos | Ordens abstratas, redes, pontos fixos |
| polígonos | Polígonos bidimensionais |
| polígono_merge | Mesclar polígonos bidimensionais sem gerar furos |
| poder | Função Generalized Power (sem ln/exp) |
| probabilidade | Teoria da probabilidade |
| PVS0 | Formalização de conceitos fundamentais de computabilidade |
| pvsio_utils | Adições ao PVSio, uma biblioteca padrão PVS para animação de especificações PVS |
| reais | Somatórios, sup, inf, sqrt sobre reais, valor absoluto, etc. |
| Riemann | Integral de Riemann |
| Scott | Topologia Scott |
| série | Séries de potências, teste de comparação, teste de razão, teorema de Taylor |
| conjuntos_aux | Conjuntos de potências, ordens, cardinalidade sobre conjuntos infinitos. Inclui fatos funcionais e relacionais baseados no Axioma da Escolha e relações de refinamento baseadas em relações de equivalência |
| formas | Formas 2D: triângulo, paralelogramo, retângulo, segmento circular |
| conjunto_sigma | Somatórios sobre conjuntos infinitos contáveis |
| classificação | Algoritmos de classificação |
| estruturas | Matrizes limitadas, sequências finitas, sacos e várias outras estruturas |
| Ataque | Formalização do teorema de Sturm para polinômios univariados. Inclui estratégias sturm e mono-poly para provar automaticamente relações polinomiais univariadas em um intervalo real |
| Tarski | Formalização do teorema de Tarski para polinômios univariados. Inclui estratégia tarski para provar automaticamente sistemas de relações polinomiais univariadas na linha real |
| topologia | Continuidade, homeomorfismos, espaços conectados e compactos, conjuntos/funções de Borel |
| trigonometria | Trigonometria: definições, identidades, aproximações |
| TRS | Sistemas de reescrita de termos e algoritmo de unificação de Robinson |
| TU_games | Jogos TU cooperativos |
| vect_análise | Limites, continuidade e derivadas de funções vetoriais |
| vetores | Vetores 2-D, 3-D, 4-D e n-dimensionais |
| enquanto | Semântica para a linguagem de programação Enquanto |
NASALib também fornece uma coleção de scripts que automatiza diversas tarefas.
proveit (*) - Executa PVS em modo batchprovethem (*) - Executa proveit em diversas bibliotecaspvsio (*) – Utilitário de linha de comando para executar o avaliador de solo PVSio.prove-all - Executa proveit em cada biblioteca no NASALib agrupando provethem para fornecer um tipo específico de execução.cleanbin-all - Limpe .pvscontext e arquivos binários das bibliotecas PVS.find-all - Pesquisa strings que correspondem a determinadas expressões regulares em bibliotecas PVS.dependencygraph - Gera um gráfico de dependência de biblioteca para bibliotecas no diretório atual.dependency-all - Gera os gráficos de dependência para as bibliotecas PVS na pasta atual.Clique aqui para obter mais detalhes sobre esses scripts.
(*) Já incluído na distribuição PVS 7.1.
NASALib (v7.0.1) é totalmente compatível com VSCode-PVS, uma interface gráfica moderna para PVS baseada em Visual Studio Code. A versão mais recente do NASALib pode ser instalada a partir do VSCode-PVS.
Para usuários avançados do PVS, a versão de desenvolvimento está disponível no GitHub. Para clonar a versão de desenvolvimento, digite o seguinte comando dentro do diretório onde o PVS 7.0 está instalado. Doravante, esse diretório será referido como
$ git clone http://github.com/nasa/pvslib nasalib O comando acima colocará uma cópia da biblioteca no diretório
Os groups de bibliotecas agora estão obsoletos . A biblioteca group foi integrada à algebra . Um link simbólico ainda é fornecido para compatibilidade com versões anteriores, mas seu uso é desencorajado. Cada menção a groups deve ser substituída por algebra .
A biblioteca trig_fnd agora está obsoleta . Ainda é fornecido para compatibilidade com versões anteriores, mas deve ser substituído por trig . A nova biblioteca trig , que costumava ser axiomática, agora é fundamental. No entanto, em contraste com trig_fnd , as definições trigonométricas são baseadas em séries infinitas, em vez de integrais. Esta mudança reduz consideravelmente a verificação de tipo de teorias envolvendo funções trigonométricas. A mudança de trig_fnd para trig não deve ter um grande impacto nos seus desenvolvimentos formais, uma vez que os nomes das definições e dos lemas são os mesmos. No entanto, a importação de teoria pode ser um pouco diferente.
Os desenvolvimentos PVS TCASII , WellClear e DAIDALUS agora estão disponíveis como parte da distribuição GitHub WellClear. O desenvolvimento PVS PRECiSA agora está disponível como parte da distribuição GitHub PRECiSA. O desenvolvimento do PVS PolyCARP agora está disponível como parte da distribuição GitHub PolyCARP.
As instruções a seguir assumem que NASALib está localizado no diretório
PVS_LIBRARY_PATH Caso não exista, cria tal variável e com o caminho deste diretório apenas como conteúdo. Geralmente é muito útil ter seus sistemas shell criando esta variável na inicialização. Para esse fim, e dependendo do seu shell, você pode adicionar uma das seguintes linhas ao seu script de inicialização. Para shell C (csh ou tcsh), você pode adicionar esta linha em ~/.cshrc :
setenv PVS_LIBRARY_PATH " /nasalib " Para Borne Shell (bash ou sh), adicione esta linha em ~/.bashrc ou ~/.profile :
export PVS_LIBRARY_PATH= " /nasalib " Se você teve uma instalação anterior do NASALib, remova o arquivo ~/.pvs.lisp ou, se você tiver uma configuração especial nesse arquivo, remova a seguinte linha
( load " /nasalib/pvs-patches.lisp " ) Por fim, vá para o diretório
O comando install-scripts atualizará e instalará scripts NASALib conforme necessário.
$ ./install-scriptsVersões mais antigas do NASALib estão disponíveis em http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
A NASALib cresceu ao longo dos anos graças à contribuição de diversas pessoas, entre elas:
Se atribuímos incorretamente um desenvolvimento PVS ou se você contribuiu para NASALib e seu nome não está incluído aqui, informe-nos.
Se você quiser contribuir, leia este guia.
NASALib é uma coleção de especificações formais, muitas das quais são de domínio público há vários anos. A Equipe de Métodos Formais do LaRC da NASA ainda mantém esses desenvolvimentos. Para os desenvolvimentos originalmente feitos pela Equipe de Métodos Formais, esses desenvolvimentos são considerados pesquisas fundamentais que não constituem software. Contribuições feitas por terceiros podem ter licenças específicas, que estão listadas no arquivo top.pvs em cada respectivo diretório. Em caso de dúvida, entre em contato com os desenvolvedores de cada contribuição, que também estão listados nesse arquivo.
Os patches PVS, incluídos no diretório pvs-patches , fazem parte do código-fonte do PVS e são cobertos pela licença de código aberto do PVS.
Algumas estratégias de prova requerem ferramentas de pesquisa de terceiros, por exemplo, MetiTarski e Z3. Por conveniência, eles estão incluídos neste repositório com permissão de seus autores. Licenças para essas ferramentas também estão incluídas conforme apropriado.
Apreciá-lo.
A Equipe de Métodos Formais do LaRC
César Muñoz Mariano Moscato
