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
| Identifer | oai:union.ndltd.org:upv.es/oai:riunet.upv.es:10251/11003 |
| Date | 10 June 2011 |
| Creators | Alarcón Jiménez, Beatriz |
| Contributors | Lucas Alba, Salvador, Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació |
| Publisher | Universitat Politècnica de València |
| Source Sets | Universitat Politècnica de València |
| Language | English |
| Detected Language | Spanish |
| Type | info:eu-repo/semantics/doctoralThesis, info:eu-repo/semantics/acceptedVersion |
| Source | Riunet |
| Rights | http://rightsstatements.org/vocab/InC/1.0/, info:eu-repo/semantics/openAccess |
Page generated in 0.0023 seconds