- -

Towards a Framework for Proving Termination of Maude Programs

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Towards a Framework for Proving Termination of Maude Programs

Show simple item record

Files in this item

dc.contributor.advisor Lucas Alba, Salvador es_ES
dc.contributor.author Alarcón Jiménez, Beatriz es_ES
dc.date.accessioned 2011-06-10T08:55:54Z
dc.date.available 2011-06-10T08:55:54Z
dc.date.created 2011-05-26T08:00:00Z es_ES
dc.date.issued 2011-06-10T08:55:40Z es_ES
dc.identifier.uri http://hdl.handle.net/10251/11003
dc.description.abstract 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. es_ES
dc.language Inglés es_ES
dc.publisher Universitat Politècnica de València es_ES
dc.rights Reserva de todos los derechos es_ES
dc.source Riunet
dc.subject Termination es_ES
dc.subject Maude es_ES
dc.subject Innermost context-sensitive rewriting es_ES
dc.subject Equational attributes es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Towards a Framework for Proving Termination of Maude Programs
dc.type Tesis doctoral es_ES
dc.identifier.doi 10.4995/Thesis/10251/11003 es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Alarcón Jiménez, B. (2011). Towards a Framework for Proving Termination of Maude Programs [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/11003 es_ES
dc.description.accrualMethod Palancia es_ES
dc.type.version info:eu-repo/semantics/acceptedVersion es_ES
dc.relation.tesis 3551 es_ES


This item appears in the following Collection(s)

Show simple item record