Redaktionell: Unviersidad Complutense de Madrid, Servicio de Publicaciones
Abteilung: Fac. de Informática - Depto. de Sistemas Informáticos y Computación
ISBN: 978-84-695-1107-7
CDU: 004.42.048(043.2)
Notes: Tesis de la Universidad Complutense de Madrid, Facultad de Informática, Departamento de Sistemas Informáticos y Computación, leída el 15-06-2011
Abstrakt: We show in this guide how to use our declarative debugger for Maude specifications. Declarative debugging is a semi-automatic technique that starts from a computation considered incorrect by the user (error symptom) and locates a program fragment responsible for the error by asking questions to an external oracle, which is usually the user. In our case the debugging tree is obtained from a
proof
tree in a suitable semantic calculus; more concretely, we abbreviate the proof trees obtained from this calculus in order to ease and shorten the debugging process while preserving the correctness and completeness of the technique.
We present the main features of our tool, what is assumed about the modules introduced by the user, the list of available commands, and the kinds of questions used during the debugging process. Then, we use several examples to illustrate how to use the debugger. We refer the interested reader to the webpage http://maude.sip.ucm.es/debugging, where these and other examples can be found together with more information about the theory underlying the debugger, its implementation and the Maude source files.
Abstrakt: We introduce a declarative debugger for Maude functional modules, which correspond to executable specifications in membership equational logic. First we describe the construction of appropriate debugging trees for oriented equational and membership inferences. These trees are obtained as the result of collapsing in proof trees all
those nodes whose correction does not need any justification.
Since
Maude supports the reflective features in its underlying logic, it includes a predefined META-LEVEL module providing access to metalevel concepts such as specifications or computations as usual data. This allows us to generate and navigate the debugging tree of a Maude computation using operations in Maude itself. Even the
user interface of the declarative debugger for Maude can be specified in Maude itself. We describe in detail this metalevel implementation of our tool.
Finally, we include several extended examples to illustrate the use of the declarative debugger and its main features, such as two different strategies to traverse the
debugging tree, use of a correct module to reduce the number of questions asked to the user, selection of trusted vs. suspicious statements by means of labels, and trusting of statements “on the fly.”
Abstrakt: We introduce a declarative debugger for Maude modules: functional modules correspond to executable specifications in membership equational logic, while system modules correspond to rewrite theories. First we describe the construction of appropriate debugging trees for oriented equational and membership inferences and rewrite rules. These trees are obtained as the result of collapsing in
proof
trees all those nodes whose correction does not need any justification.
We include several extended examples to illustrate the use of the declarative debugger and its main features, such as two possible constructions of the debugging tree, two different strategies to traverse it, use of a correct module to reduce the number of questions asked to the user, selection of trusted vs. suspicious statements by means of labels, and trusting of statements “on the fly.”
Since Maude supports the reflective features in its underlying logic, it includes a predefined META-LEVEL module providing access to metalevel concepts such as specifications or computations as usual data. This allows us to generate and navigate the debugging tree of a Maude computation using operations in Maude itself. Even the user interface of the declarative debugger for Maude can be specified in Maude itself. We describe in detail this metalevel implementation of our tool.
Abstrakt: Rewriting logic is a logic of change, where rewrites correspond to transitions between states. One of the main characteristics of these transitions is that they can be nondeterministic, that is, given an initial state, there is a set of possible reachable states. Thus, an additional problem when debugging rewrite systems is that, although all the terms obtained could be correct, it is possible that not all the
desired terms are computed, i.e., there are missing answers.
We propose a calculus that allows to infer, given an initial term, the complete set of reachable terms. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers, whose adequacy for debugging is proved. We apply then this method to Maude specifications, a high-performance system based on rewriting logic, adding many options to build and navigate the tree. Several examples are shown to illustrate the use of the
debugger and all of its features.
Since Maude supports the reflective features in its underlying logic, it includes a predefined META-LEVEL module providing access to metalevel concepts such as specifications or computations as usual data. This allows us to generate and navigate the debugging tree using operations in Maude itself. Even the user interface of the declarative debugger for Maude can be specified in Maude itself.
We also describe in detail this metalevel implementation of our tool.
Abstrakt: Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows to state membership axioms characterizing the elements
of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. We propose here a calculus to infer reductions, sort inferences, normal forms and least sorts with the equational part, and rewrites and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for both wrong (an incorrect result obtained from an initial result) and missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.
Abstrakt: We explore the features of rewriting logic and its language Maude as a logical and semantic framework for representing both the semantics of CCS, and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics was given in [MOM93], it cannot be directly executed in the current default interpreter of Maude. Moreover, it cannot be
used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved by exploiting the reflective properties of rewriting logic, which allow controlling the rewriting process. We also show how the semantics can be extended to traces of actions and to the CCS weak transition relation. This executable specification plus the reflective control of the rewriting process can be used to analyze CCS processes.
Abstrakt: El proyecto es un estudio sobre el modelado de procesos de negocio (BPM) donde se describen las partes en las que debe componerse una arquitectura o cómo hacer uso de patrones durante el diseño de los procesos. También analiza las técnicas y estándares más destacados que hay en la actualidad. Por otra parte, del lenguaje Maude se hace una
introducción a los tipos de módulos necesarios para poder definir especificaciones de datos. Al final
ambos conceptos, BPM y Maude, se ven relacionados a través de la
notación gráfica BPMN y de las estrategias de Maude, que cómo se verá son dos maneras de controlar el comportamiento de los procesos. Nuestra propuesta es realizar una aproximación a través de la correspondencia entre los símbolos de la notación y las estrategias que dirigen las reglas del sistema. Se incluye un ejemplo sobre catalogación
y consulta de artículos donde se puede ver esta relación, llamado Portal de Revistas Complutenses.
[ABSTRACT]
This is a project about the business process modeling (BPM), where the different parts that any architecture should contain are described. It is also explained how to use the patterns during the design of the process and the most common techniques and standards which we have nowadays. Besides there is an introduction to the types of
modules that we need to define our data specifications. In the end both concepts, BPM and Maude, are related by the graphic notation BPMN and the Maude strategies, which
conform, as we will see, two different options to control the behavior of the process. Our intention is to relate them through the correspondence between the symbols of the
notation and the strategies which lead the rules of the system. It is also included an example called “Portal de Revistas Complutenses” about catalog and search of articles
where this relationship can be observed.
Notes: Máster en Investigación en Informática, Facultad de Informática, Departamento de Ingeniería del Software e Inteligencia Artificial, curso 2008-2009
Abstrakt: La lógica de reescritura, propuesta por José Meseguer en 1990 como marco de unificación de modelos de computación concurrente, es una lógica para razonar sobre sistemas concurrentes con estado que evolucionan por medio de transiciones. Desde su definición, se ha propuesto a la lógica de reescritura como marco lógico y semántico en el cual poder expresar de forma natural otras muchas lógicas, lenguajes y modelos de computación. Además,
la lógica de reescritura es ejecutable utilizando el lenguaje multiparadigma Maude cuyos módulos son teorías en la lógica de reescritura. El objetivo principal de esta tesis es extender la idea de la lógica de reescritura y Maude como marco semántico a la idea de marco semántico ejecutable. Este objetivo se ha abordado desde diferentes puntos de vista. En primer lugar, presentamos representaciones ejecutables de semántica operacionales estructurales. En concreto, hemos estudiado dos implementaciones diferentes de la semántica de CCS y su utilización para implementar la lógica modal de Hennessy-Milner; hemos realizado una implementación de una semántica simbólica para LOTOS incluyendo especificaciones de tipos de datos en ACT ONE que son traducidos a módulos Maude y de una herramienta que permite al usuario ejecutar directamente sus especificaciones LOTOS; y hemos utilizado las mismas técnicas para implementar otros tipos de semánticas operacionales de lenguajes funcionales e imperativos sencillos, incluyendo tanto semánticas de evaluación (o paso largo) como semánticas de computación (o paso corto). En segundo lugar, hemos querido contribuir al desarrollo de una metodología propuesta recientemente por Denker, Meseguer y Talcott para la especificación y análisis de sistemas basada en una jerarquía de métodos incrementalmente más fuertes, especificando y analizando tres descripciones ejecutables del protocolo de elección de líder dentro de la especificación del bus multimedia en serie IEEE 1394 (conocido como "FireWire"). En dos de estas descripciones hacemos especial énfasis en los aspectos relacionados con el tiempo, esenciales para este protocolo. Por último, hemos abordado la dotación de semántica formal a lenguajes de la web semántica, mediante la traducción del lenguaje de descripción de recursos web RDF (Resource Description
Framework) a Maude y su integración con Mobile Maude, una extensión de Maude para permitir cómputos móviles.
Stichwort: Lenguajes de programación Semántica Tesis En línea
Redaktionell: Universidad Complutense de Madrid, Servicio de Publicaciones
Abteilung: Fac. de Informática - Depto. de Sistemas Informáticos y Computación
ISBN: 84-669-1853-1
CDU: 519.767(043.2)
Notes: Tesis de la Universidad Complutense de Madrid, Facultad de Informática, Departamento de Sistemas Informáticos y Programación, leída el 24-03-2003
