Please use this identifier to cite or link to this item: http://repositorio.unb.br/handle/10482/23406
Title: Formalização da terminação de especificações funcionais
Authors: Ramos, Thiago Mendonça Ferreira
Orientador(es):: Ayala-Rincón, Mauricio
Assunto:: Terminação móvel
Programação (Computadores)
Turing
Issue Date: 27-Apr-2017
Data de defesa:: 2-Mar-2017
Citation: 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.
Abstract: 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.
???metadata.dc.description.abstract1???: 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.
Description: Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2017.
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.
Appears in Collections:CIC - Mestrado em Informática (Dissertações)

Files in This Item:
File Description SizeFormat 
2017_ThiagoMendonçaFerreiraRamos.pdf601.05 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.