Formalização da automação da terminação através de grafos com matrizes de medida

Abstract

Uma nova estrutura baseada em digrafos e denominada Grafos com Matrizes de Medida (MWGs) é apresentada. Esta estrutura se baseia na estrutura conhecida como Grafos de Contextos de Chamado (CCGs) e é aplicada na verificação de terminaçãao de programas funcionais de primeira-ordem especificados no estilo da linguagem de especifica¸cao do as- sistente de prova PVS. Similarmente a CCGs, os vértices em um MWG correspondem aos chamados recursivos da função modelada. Caminhos em um MWG, assim como em um CCG, representam o fluxo de execução dos chamados recursivos do programa em questão. De acordo com o princípio de mudança de tamanho, MWGs são aplicados na verificação de terminação através da especificação de critérios para garantir que todos os circuitos no MWG, que corresponderiam a possíveis execuções infinitas de chamados recursivos, nao podem ser repetidos infinitamente. Em CCGs, isto é realizado através da construção de combinação de medidas, sobre o domínio de uma relação bem-fundada, definidas nos parâmetros da função recursiva que está sendo modelada. Assim, a fim de verificar terminação da função, deve-se verificar que a combinação de medidas decresce estritamente em todos os possíveis circuitos. Ao invés de procurar uma combinação de medidas para cada circuito, em MWGs as arestas são rotuladas com matrizes quadradas cujas entradas expressam relaçoes entre diferentes medidas aplicadas aos parâmetros formais e atuais. Desta forma, o comportamento das medidas após executar uma sequência de chamados recursivos associada a um caminho no MWG é expresso através da multiplicação especializada das matrizes que rotulam as arestas do caminho. O critério de terminação em MWG corresponde a uma simples noção de positividade da matrix associada a um determinado circuito. As matrizes de medida modelam o resultado das combinações de medidas da tecnologia CCG de uma forma muito elegante possibilitando a formulação de critérios simples de terminação em MWGs. Tais critérios baseiam-se na positividade dos ciclos (circuitos simples) do MWG, levando a positividade de qualquer circuito. Dois critérios de terminação para MWGs são formalizados. A correspondência entre terminação em CCGs e MWGs é formalizada. A especificação de uma simples linguagem funcional de primeira-ordem com sua respectiva semântica para terminação é apresentada, e são discutidos os elementos necessários para a formalizaçao da correspondência entre a semântica de terminação para esta linguagem e terminação em MWGs. _____________________________________________________________________________ ABSTRACT

A new digraph structure called Matrix-Weigthed Graphs (MWGs) is presented. This structure is based on Calling Context Graphs (CCGs) and is applied to verify termination of first-order functional programs written in the style of the specification language of the PVS proof assistant restricted to its first-order fragment. Similarly to CCGs, a MWG has nodes that correspond to the recursive calls of the modeled program. Paths in a MWG, as well as in a GCC, model the execution ow of recursive calls in the associated program. According to the size-change termination principle, MWGs are used to verify termination of the specification through criteria that guarantee that all circuits in the MWG, would correspond to possible infinite executions of recursive calls, can not be repeated infinitely. In CCG, this is done by building well-founded measures for the parameters of the recursive functions that should be proved to strictly decreasing in all possible circuits. Instead searching a combination of measures for any circuit that guarantees the impossibility of infinite recursive calls as done in CCGs, MWGs edges are labelled with square matrices whose components express relations between different measures applied to the formal and actuals parameters. In this way, the behavior of measures after executing the recursive calls associated to a path in the MWG is expressed by an specialized multiplication of the matrices labeling the edges in the path. The termination criterion in the MWG corresponds to a simple notion of positivity of the matrix associated to a given circuit. The measure matrices model the results of combination of measures of the CCG's technology in a very elegant manner making possible the formulation of simple termination criteria in MWGs. Such criteria is based on the positivity of the cycles (simple circuits) of the MWG, leading to positivity of any circuit. Two termination criteria for MWG are formalized. The correspondence between the termination in CCGs and MWGs is formalized. The specification of a simple first-order language with its semantics for termination is presented and the necessary elements to formalize the correspondence between the semantics of termination of this language and termination in MWGs.