Maude es un lenguaje de programación declarativo basado en la lógica de reescritura que incorpora muchas características que lo hacen muy potente. Sin embargo, a la hora de probar ciertas propiedades computacionales esto conlleva dificultades. La tarea de probar la terminación de sistemas de reesctritura es de hecho bastante dura, pero aplicada a lenguajes de programación reales se concierte en más complicada debido a estas características inherentes. Esto provoca que métodos para probar la terminación de este tipo de programas requieran técnicas específicas y un análisis cuidadoso. Varios trabajos han intentado probar terminación de (un subconjunto de) programas Maude. Sin embargo, todos ellos siguen una aproximación transformacional, donde el programa original es trasformado hasta alcanzar un sistema de reescritura capaz de ser manejado con las técnicas y herramientas de terminación existentes. En la práctica, el hecho de transformar los sistemas originales suele complicar la demostración de la terminación ya que esto introduce nuevos símbolos y reglas en el sistema. En esta tesis, llevamos a cabo el problema de probar terminación de (un subconjunto de) programas Maude mediante métodos directos. Por un lado, nos centramos en la estrategia de Maude. Maude es un lenguaje impaciente donde los argumentos de una función son evaluados siempre antes de la aplicación de la función que los usa. Esta estrategia (conocida como llamada por valor) puede provocar la no terminación si los programas no están escritos cuidadosamente. Por esta razón, Maude (en concreto) incorpora mecanismos para controlar la ejecución de programas como las anotaciones sintácticas que están asociadas a los argumentos de los símbolos. En reescritura, esta estrategia sería conocida como reescritura sensible al contexto innermost (RSCI). Por otro lado, Maude también incorpora la posibilidad de declarar atributos. / Alarcón Jiménez, B. (2011). Towards a Framework for Proving Termination of Maude Programs [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/11003

Établir des preuves de bon fonctionnement des programmes est délicat ; on a recours à des outils de preuve, qui doivent procéder par surapproximation (à cause du théorème de Rice). La complétion d'automate est un tel outil, qui surapproxime l'ensemble des termes accessibles lors de l'exécution d'un programme représenté par un système de réécriture. La stratégie d'évaluation donne l'ordre dans lequel les sous-termes d'un terme doivent être réécrits ; en tenir compte permet une meilleur précision de l'analyse. Notre thèse propose une adaptation de la complétion d'automate à la stratégie en profondeur, utilisée notamment par OCaml. Nous établissons la correction et la précision de notre méthode et montrons comment elle s'inscrit dans le cadre plus large de l'analyse de programmes fonctionnels (OCaml). / Proving that programs behave correctly is difficult; one uses proof tools, which must rely on overapproximation (because of Rice's theorem). Automaton completion is such a tool, which overapproximates the set of reachable terms during the execution of a program represented as a TRS. An evaluation strategy dictates which subterm of a term should be rewritten first; taking this into account allows for a better approximation. Our thesis sets forward an adaptation of automaton completion to the innermost strategy, which is used among others by OCaml. We prove the soundness and the precision of our adaptation and show how it is part of a greater framework for analysis of functional programms (OCaml).

Made available in DSpace on 2016-04-25T19:20:34Z (GMT). No. of bitstreams: 1 Adailson Nascimento Souza.pdf: 786423 bytes, checksum: 41b0fcf10d370e2d25783a689ad8263e (MD5) Previous issue date: 2014-12-05 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The current dissertation investigates the knowledge of God as My Innermost Self in the memory, having as reference the Confessions, book X. Following the Augustinian view, here we intend to analyze which is the type of knowledge possible to men, and where to find it. For the Bishop of Hippo, only through the foundation of the christian faith a knowledge of God would be accessible. Considering the studied book, that access will be possible when a path in the memory is traversed, based in three actions - one exterior, another interior, and finally a superior. It is through these actions that the human being could know God in his most intimate place that we do not know of, but that exists inside every single men. By making use of authors such as Johannes Brachtendorf, Peter Brown, Philoteus Boehner and Joel Gracioso, this research seeks to concentrate in the referred question, tracing in an objective way all biographic influences that inspired Saint Augustine to achieve his conviction that God is more Intimate of me than I am of Him / A presente dissertação investiga o conhecimento de Deus como Íntimo Meu na memória, tomando como referência o livro X das Confissões. Seguindo a visão agostiniana, aqui pretendemos analisar qual o tipo de conhecimento possível ao homem, e onde encontrar tal conhecimento. Para o bispo de Hipona, somente através da fundamentação da fé cristã seria acessível um conhecimento de Deus. De acordo com o livro referido, esse acesso será possível quando for realizada uma trajetória na memória pautada em três ações - uma exterior, uma interior, e uma superior. Fazendo uso dessas ações é que o ser humano poderia conhecer a Deus no lugar mais íntimo e que desconhecemos, mas que existe dentro de cada um. Acolhendo como norte teórico autores como Johannes Brachtendorf, Peter Brown, Philoteus Boehner e Joel Gracioso, esta pesquisa procura se concentrar na referida questão, traçando de forma objetiva as influências biográficas que contribuíram para que Santo Agostinho pudesse chegar à sua convicção de que Deus é mais Íntimo de mim, do que eu sou d‟Ele

農林水産研究情報センターで作成したPDFファイルを使用している。