On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS
| Autor: | Almeida, Ariane Alves |
|---|---|
| Přispěvatelé: | Muñoz, César Augusto, Ayala-Rincón, Mauricio |
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | Repositório Institucional da UnB Universidade de Brasília (UnB) instacron:UNB |
| Popis: | Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2021. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES). Embora indecidível, terminação é uma propriedade muito importante relacionada à cor- reção de objetos computacionais. Ela garante que para cada entrada, não haverá execução infinita, ou seja, a execução deve parar e fornecer algum resultado. Esta propriedade per- mite, por exemplo, raciocinar sobre a correção de programas, uma vez que garantir que alguma propriedade seja válida para cada saída depende da obtenção de uma saída a ser verificada sempre que uma entrada for fornecida. Ao longo dos anos, várias estratégias de semidecisão foram usadas para abordar esse problema e raciocinar sobre ele. No contexto de Programas Funcionais (FPs), por exemplo, a análise pode ser feita por meio dos Gráfi- cos de Contexto de Chamada, e no contexto de Sistemas de Reescrita de Termos (TRSs), podem ser usados Pares Dependentes. Este trabalho formaliza o Critério de Terminação por Pares Dependentes (Mais Inter- nos), um critério muito conhecido para análise de terminação de TRSs, no assistente de prova PVS. PVS é um assistente de prova com uma linguagem de especificação funcional que permite lógica de ordem superior e realiza provas seguindo o Cálculo de Sequentes de Gentzen. Também são apresentados vários Critérios de terminação formalizados para FPs em uma linguagem simplificada que modela especificações em PVS (chamada PVS0) e a formalização da equivalência entre eles, permitindo automação de provas de terminação de especificações de funções recursivas de primeira ordem em PVS. O trabalho também discute a possibilidade de navegar entre os critérios de terminação para TRSs e FPs com o objetivo de aprimorar a automação para verificar terminação. Although undecidable, termination is a very important property related to the correct- ness of computational objects. It ensures that for every input, there will be no infinite execution, i.e., the execution must stop and provide some result. This property allows, for instance, reason about correctness of programs, since to guarantee that some prop- erty hold for every output depends on obtaining an output to be analysed whenever an input is provided. Through the years, several semi-decision strategies have been used to address such problem and reason over it. In the context of Functional Programs (FPs), for instance, the analysis can be done through the Calling Context Graphs, and in the context of Term Rewriting Systems (TRSs), Dependency Pairs can be used. This work formalizes the (Innermost) Dependency Pairs Termination Criterion, a very well-known criteria for analyzing termination of TRSs, in the proof assistant PVS. PVS is a proof assistant with a functional specification language that allows higher order logic and performs proofs following the Gentzen Calculus of Sequents. It is also presented several termination criteria formalized for FPs in a simplified language modeling PVS specifications (called PVS0) and the formalization of the equivalence between them, al- lowing automation for proving termination of recursive functions first-order specification in PVS. The work also discusses the possibility of navigating between the termination criteria for TRSs to FPs aiming to improve automation of verification for termination. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|