Skip navigation
Use este identificador para citar ou linkar para este item: http://repositorio.unb.br/handle/10482/23406
Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
2017_ThiagoMendonçaFerreiraRamos.pdf601,05 kBAdobe PDFVisualizar/Abrir
Título: Formalização da terminação de especificações funcionais
Autor(es): Ramos, Thiago Mendonça Ferreira
Orientador(es): Ayala-Rincón, Mauricio
Assunto: Terminação móvel
Programação (Computadores)
Turing
Data de publicação: 27-Abr-2017
Referência: RAMOS, Thiago Mendonça Ferreira. Formalização da terminação de especificações funcionais. 2017. viii, 82 f., il. Dissertação (Mestrado em Informática)—Universidade de Brasília, Brasília, 2017.
Resumo: Terminação é uma propriedade crítica para formalização de correção de programas. Verificar automaticamente terminação de um programa é conhecido como Problema da Parada e Turing provou que é um problema indecidível. Apesar disso, é possível construir algoritmos de semi decisão para verificar terminação, que respondem ‘sim’ se pode provar que o algoritmo para e ‘não sei’ caso contrário. Para construir esses algoritmos de semi decisão é necessário considerar diferentes noções de terminação, provando que são equivalentes. Neste trabalho, noções de terminação são formalizadas equivalentes para uma linguagem funcional de primeira ordem chamada PVS0 usando o assistente de prova Prototype Verification System. Essas noções são: as funções produzem uma saída, a árvore de derivação de chamados recursivos de funções tem tamanho finito (ambas as noções são chamadas terminação semântica), e os argumentos das funções decrescem para cada chamado recursivo (essa noção é chamada ranking function). As contribuições desse trabalho incluem a formalização de alguns lemas necessários para demonstrar equivalência entre noções de terminação semântica e ranking function, e como resultado principal a formalizações de indecidibilidade do Problema da Parada e Turing-Completude de PVS0.
Abstract: Termination is a critical property for the formalization of programs correctness. Verifing automatically termination of a program for an input is known as Halting Problem and Turing proved that this is undecidable. However, it is possible to build semi decision algorithms for the verification of termination, that answer ‘yes’ if it is possible to prove that the algorithm halts, and ‘do not know’ otherwise. To construct these semi decision algorithms it is necessary to consider different notions of termination, proving that they are equivalent. In this work, notions of termination were formalized equivalent for a minimal functional first order language called PVS0 using the proof assistant Prototype Verification System. These notions are: the functions produces an output, the derivation tree of recursive calls of functions has a finite size (both these notions are called semantic termination), and the arguments of functions decreases for each recursive call (this notion is called ranking function). The contributions of this work includes formalization of lemma related with the equivalence between notions of semantic and ranking function termination, and the main results are the formalization of indecidability of Halting Problem and Turing-Completeness of PVS0.
Unidade Acadêmica: Instituto de Ciências Exatas (IE)
Departamento de Ciência da Computação (IE CIC)
Informações adicionais: Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2017.
Programa de pós-graduação: Programa de Pós-Graduação em Informática
Licença: A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.
DOI: http://dx.doi.org/10.26512/2017.03.D.23406
Aparece nas coleções:Teses, dissertações e produtos pós-doutorado

Mostrar registro completo do item Visualizar estatísticas



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.