IV Jornadas sobre Programación y Lenguajes
11-12 Noviembre 2004
Málaga

 Español English

• Analysing Definitional Trees
• Pascual Julián-Iranzo y Christian Villamizar-Lamus

Categoría: 4 (Trabajo ya publicado - FLOPS´04)

Resumen:
This paper describes how high level implementations of (needed) narrowing into Prolog can be improved by analysing definitional trees. First, we introduce a refined representation of definitional trees that handles properly the knowledge about the inductive positions of a pattern. The aim is to take advantage of the new representation of definitional trees to improve the aforementioned kind of implementation systems. Second, we introduce selective unfolding transformations, on determinate atom calls in the Prolog code, by examining the existence of what we call deterministic (sub)branches´ in a definitional tree. As a result of this analysis, we define some generic algorithms that allow us to compile a functional logic program into a set of Prolog clauses which increases determinism and incorporates some refinements that are obtained by {\em ad hoc\/} artifices in other similar implementations of functional logic languages. We also present and discuss the advantages of our proposals by means of some simple examples.

Palabras clave: Functional logic programming, narrowing strategies, implementation of functional logic languages, program transformation.

• A First-Order Functional Language for Reasoning about Heap Consumption

Ricardo Peña y Clara Segura

Categoría: 5 (Trabajo en progreso)

Resumen:
Most functional languages abstract the programmer from the details of the memory management done by his/her program at run time. This model is acceptable in most situations, being its main advantage that programmers are not bored, and programs are not obscured, with low level details about memory management. But in some other contexts like real-time programs or safety critical applications, time delays due to garbage collection or abortion due to memory exhaustion are not acceptable. On the other hand, many imperative languages offer low level mechanisms to allocate and free heap memory which give the programmer a complete control over memory usage, but without any safety requirement. We have chosen a semi-explicit approach by defining a functional language in which the programmer cooperates with the memory management system by providing some information about the intended use of data structures. For instance, he/she may indicate that some particular data structure will not be needed in the future and, as a consequence, it may be safely destroyed by the runtime system and its memory recovered. The language also allows to control the degree of sharing between different data structures. A type system guarantees that the explicit memory management is done in a safe way. In particular, it guarantees that a destroyed object is never referenced again and that garbage is always recovered. The final aim of the system is to reason about the memory consumed by a program.

Palabras clave: functional programming, memory management, static analysis, type systems.

• Tagged systems: a homogeneous framework for the specification of historical-context dependent properties

Fernando Rosa Velardo, David de Frutos Escrig y Clara Segura Díaz

Categoría: 1 (Trabajo original)

Resumen:
We propose a general method for the treatment of history-dependant runtime errors. When one has to control this kind of errors, a tagged version of the language is usually defined, in which tags capture only the necessary information of the history of processes. We will characterize such languages as being quotients of the reachability tree defined by the transition graph. This fact tells us that the property characterized by the tagged language is indeed a property of the original one, thus maintaining an homogeneous framework instead of defining an ad hoc semantics for each property. In particular, we could still use the analysis machinery existing in the calculus in order to prove that or other related properties. We have applied this methodology to the study of resource access control in a distributed pi-calculus, called Dpi. In particular, we have proved that the tagged version of Dpi is a tagging according to our definition.

Palabras clave: operational semantics, type systems for security, mobile calculus.

• Proving modal properties of rewrite theories using Maude´s metalevel

Isabel Pita y Miguel Palomino

Categoría: 1 (Trabajo original)

Resumen:
Rewriting logic provides a formal framework for modelling concurrent systems in terms of states and state transitions. It is a logic of change in which deduction directly corresponds to the change. In contrast, the Verification Logic for Rewriting Logic (VLRL) is an action modal logic to talk about change in a more indirect and global manner, like other modal and temporal logics. VLRL was developed to prove abstract properties of systems specified in rewriting logic. In VLRL, rewrite rules are captured as actions, transitions are represented by action modalities, and the structure of the state is represented by spatial modalities. In this way, action modalities allow the definition of properties of states after a particular sequence of rewrites, and the spatial modality allows the definition of properties of components of the state. In this paper we develop a method to prove that a given VLRL formula holds in a state. To obtain the resulting state of executing an action on a state we use the reflective capabilities of rewriting logic. Reflection allows a system to access its own metalevel, providing a powerful mechanism for controlling the rewriting process. Maude metalevel provides convenient operations that permit us to control the execution of rewrite rules in the object system. Identity actions and componed actions are treated by looking to the parts of the state also with the Maude metalevel. This allows us to obtain the new states and check satisfaction of the action properties.

Palabras clave: Lógica de reescritura, Reflexión, Lógica modal, Verificación de propiedades, VLRL.

• Introducing Constraints on Sets of Spatial Objects

Jesús M. Almendros-Jiménez y Antonio Corral

Categoría: 5 (Trabajo en progreso)

Resumen:
In this paper we present a framework for handling of constraints on sets of spatial objects. For this spatial constraint system we formally define a set of spatial data types together with operations on them. We show how to formulate a spatial constraint satisfaction problem using these constraints, by means of several examples. We also study safety conditions in order to ensure that each spatial constraint satisfaction problem is equivalent to a solved form representing its set of solutions.

Palabras clave: Programación con Restricciones, Bases de Datos Espaciales.

• A tutorial on specifying data structures in Maude

Narciso Martí-Oliet, Miguel Palomino y Alberto Verdejo

Categoría: 2 (Tutorial)

Resumen:
This tutorial describes the equational specification of a series of typical data structures in Maude. We start with the well-known stacks, queues and lists, to continue with binary and search trees. Not only are the simple versions considered but also advanced ones such as AVL and 2-3-4 trees. The operator attributes available in Maude allow the specification of data based on constructors that satisfy some equational properties, like concatenation of lists which is associative and has the empty list as identity, as opposed to the free constructors available in other functional programming languages. Moreover, the expressive version of equational logic in which Maude is based, namely membership equational logic, allows the faithful specification of types whose data is defined not only by means of constructors, but also by the satisfaction of additional properties, like sorted lists or search trees. In the second part of the paper we describe the use of an inductive theorem prover, ITP, which itself is developed and integrated in Maude by means of the powerful metalevel and metalanguage features offered by the latter, to prove properties of the data structures. This is work in progress because the ITP is still under development and, as soon as the data gets a bit complex, the proof of their properties gets even more complex.

Palabras clave: Data structures, algebraic specification, membership equational logic, Maude, inductive theorem proving.

• Una Aproximación Práctica al Desarrollo de Comprobadores de Tipos basada en Patrones de Diseño

Francisco Ortin, Luis Vinuesa y Juan Manuel Cueva

Categoría: 1 (Trabajo original)

Resumen:

Palabras clave: Sistemas de tipos, comprobador de tipos, patrones de diseño, orientación a objetos.

• Agregando orden superior al lenguaje Java. Una nueva perspectiva para el diseño de métodos

Josefina Llaberia Albarrán y Silvia Clérici

Categoría: 1 (Trabajo original)

Resumen:

• Un Marco de Trabajo para la Construcción de Herramientas de Model Checking

María del Mar Gallardo, Alejandro Carmona, Jesús Martínez y Pedro Merino

Categoría: 5 (Trabajo en progreso)

Resumen:
Este artículo presenta trabajo en progreso para la obtención de un núcleo de código que permita la experimentación con estrategias para la detección automática de fallos en software para sistemas empotrados y distribuidos. El objetivo inicial es exportar nuestra experiencia en la combinación de model checking y abstracción del proyecto aSPIN.

Palabras clave: Model checking, implementación de herramientas de verificacion, marcos de trabajo.

• Una aproximación lógica a la verificación de propiedades de programas lógico-funcionales

José Miguel Cleva, Javier Leach, Francisco J. López-Fraguas

Resumen:
Este trabajo es un resumen de los trabajos desarrollados este año, donde se aborda el tema de la verificación de propiedades de programas lógico funcionales desde un punto de vista lógico. Para ello se parte de un semántica bien conocida para este tipo de lenguajes como es la proporcionada por el marco lógico CRWL, y se asocia a cada CRWL-programa un programa lógico que servirá como base para la demostración de las propiedades del programa original. Se analizan los principales inconvenientes prácticos de este enfoque y se proponen un par de refinamientos que mejoran la efectividad de la aproximación

Palabras clave: Programación lógico-funcional, verificación, programación lógica.

• Phrase Similarity through Approximate Tree Matching

Francisco José Ribadas Pena, Miguel Angel Alonso Pardo y David Cabrero Souto

Categoría: 1 (Trabajo original)

Resumen:
We describe an algorithm to measure the similarity between phrases, integrating both the edit distance between trees and single-term similarity techniques, and allowing the pattern to be defined approximately, omitting some structural details. Such a technique is of interest in a variety of applications, such as information extraction/retrieval or question answering, where error-tolerant recognition allows incomplete sentences to be integrated in the computational process. In relation to previous works, we stress the use of the grammatical underlying structure, which serves as a guide in the computation of semantic similarity between words.

Palabras clave: Reconocimiento de patrones en árboles, proximidad semántica, distancia de edición, análisis sintáctico, lenguaje natural.

• An Input/Output Semantics for Distributed Program Equivalence Reasoning

Miquel Bertran, Francesc Babot y August Climent

Categoría: 1 (Trabajo original)

Resumen:
Some notions and deduction rules needed in formal equivalence reasoning with distributed imperative programs, with synchronous communications, are introduced. Starting at the semantic framework of Manna and Pnueli, and working in their notation SPL, the notions of input/output behavior and equivalence are defined as extensions. The former records the values traversing channels, in addition to the usual state variable values. Input/output equivalence is weaker than congruence but preserves the input/output relation, or function, of modular procedures, a slight modification of the modules of Manna and Pnueli. With this equivalence, a novel set of SPL laws for practical communication elimination has been made possible. A summary of these laws, as well as an outline of an equivalence proof of a pipelined processor software model, are included as illustrations.

Palabras clave: Distributed programs, parallel programs, input/output equivalence, equivalence preserving transformations, verification, program simplification, synchronous communications, laws of distributed programs.

• Compiling Thread-Level Parallel Programs with a C-Compiler

Martti Forsell
(VTT Electronics, Finlandia)

Categoría: 1 (Trabajo original)

Resumen:
Recent advances in multithreaded shared memory architectures have created a need for efficient and easy-to-use thread-level parallel (TLP) programming languages and tools supporting the synchronous shared memory model. In our previous work we have developed e, a fine-grained TLP programming language for multiprocessor architectures realizing such a model. The language uses a familiar c-like syntax and provides support for shared and private variables, arbitrary hierarchical groups of threads, and synchronous control structures. This allows a programmer to use various advanced TLP programming techniques like data parallelism, divide-and-conquer technique, different blocking techniques, and both synchronous and asynchronous programming style. In this paper we describe how an experimental compiler for e can be set up by using a standard c-compiler. We will also shortly evaluate the compiler with real parallel programs on our scalable Eclipse network on chip architecture.

Palabras clave:

• A Lightweight Approach to Program Specialization

Claudio Ochoa, Josep Silva y Germán Vidal

Categoría: 1 (Trabajo original)

Resumen:
Within the imperative programming paradigm, program slicing has been widely used as a basis to solve many software engineering problems, like debugging, testing, differencing, specialization, and merging. In this work, we present a lightweight approach to program specialization of lazy functional logic programs which is based on dynamic slicing. The kind of specialization performed by our approach cannot be achieved with other, related techniques like partial evaluation.

Palabras clave: Functional logic programming, slicing, specialization

• Rewriting-engined Web Sites Verification

María Alpuente, Demis Ballis y Moreno Falaschi
(Universidad Politécnica de Valencia - Universitá di Udine)

Categoría: 4 (Trabajo ya publicado - RULE´04, JELIA´04)

Resumen:
{\sc Verdi} is a system for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are actually fulfilled. It provides a rule-based, formal specification language which allows us to define syntactic/semantic properties of the Web site as well as a verification facility which computes the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete/missing Web pages.

Palabras clave: Formal verification of semistructured data, specification languages, rewriting, simulation.

• Improved Tupling for Optimizing Multi-Paradigm Declarative Programs

Categoría: 4 (Trabajo ya publicado - IBERAMIA´04)

Resumen:
This paper investigates the optimization by fold/unfold of declarative programs that integrate the best features from both functional and logic programming. Transformation sequences are guided by a mixed strategy that successfully combines two well-known heuristics -composition and tupling-, thus avoiding the construction of intermediate data structures and redundant sub-computations. We have decomposed the internal structure of both methods in three low-level transformation phases in order to analyze their main similarities and differences. In particular, whereas composition is able to produce a single function definition for some nested (composed) functions, the tupling method merges non-nested functions calls into a new function definition called eureka. In our approach, we solve the non trivial problem of discovering the set of calls to be tupled in an incremental way, i.e. by iteratively chaining different eureka definitions where only non-nested calls sharing common variables are taken into account. With this easy method, that complements the one done by composition, we are able to perform powerful tupling optimizations at a very low cost. Moreover, by appropriately combining both strategies, together with a simplification pre-proccess based on a kind of normalization, we optimize a wide range of programs (with nested and/or non-nested function calls) in a fully automatic way.

Palabras clave: Functional-Logic Programming Program Optimization Fold/Unfold Transformations Composition and Tupling.

• Unfolding-based Improvements on Fuzzy Logic Programs

Pascual Julián Iranzo, Ginés Moreno Valverde y Jaime Penabad Vázquez

Categoría: 1 (Trabajo original)

Resumen:
Unfolding is a semantics-preserving program transformation technique that consists in the expansion of subexpressions of a program using their own definitions. The unfolding transformation is the basis for developing sophisticated and powerful programming tools, such as fold/unfold transformation systems and it is able to improve programs, generating more efficient code. In this paper we define two unfolding-based transformation rules (namely, fuzzy unfolding and T-Norm replacement) that extend the classical definition of the unfolding rule (for pure logic programs) to a fuzzy logic setting. We use an extremely flexible fuzzy variant of Prolog where each program clause can be interpreted under a different (fuzzy) logic. Now, the notion of fuzzy computed answer is conceived as a pair < truth degree; substitution> computed by Fuzzy SLD-Resolution. We adapt the concept of a computation rule, a mapping that selects the subexpression of a goal involved in a computation step, and we prove the independence of the computation rule. Moreover, we define a basic transformation system and we demonstrate its strong correctness properties, that is, original and transformed programs compute the same fuzzy computed answers. Finally, we prove that our transformation rules applied on a given program, always produce an improvement in the efficiency of the residual program, by reducing the length of successful Fuzzy SLD-derivations.

Palabras clave: Fuzzy Logic Programming, Program Transformation.

• Towards (constructor) normal forms for Maude within Full Maude

Francisco Durán, Santiago Escobar y Salvador Lucas

Categoría: 3 (Sistema software)

Resumen:
Maude is able to deal with infinite data structures and avoid infinite computations by using \emph{strategy annotations}. However, they can eventually make the computation of the normal form(s) of some input expressions impossible. We have used Full Maude to implement two new commands \pr{norm} and \pr{eval} which furnish Maude with the ability to compute (constructor) normal forms of initial expressions even when the use of strategy annotations together with the built-in computation strategy of Maude is not able to obtain them. These commands have been integrated into Full Maude, making them available inside the programming environment like any other of its commands. Moreover, the type of annotations allowed has been extended, giving to Maude the ability of dealing with on-demand strategy annotations, that is, negative indices that express \emph{evaluation on-demand}, where the \emph{demand} is an attempt to match an argument term with the left-hand side of a rewrite rule.

Palabras clave:

• Elimination of local variables from definite logic programs

Javier Álvez y Paqui Lucio

Categoría: 1 (Trabajo original)

Resumen:
In logic programs, a variable is said to be local if it occurs in a clause body but not in its head. It is wellknown that local variables are the main cause of inefficiency (sometimes even incompleteness) in negative goal computation. The problem is that universal quantification is unavoidable for computing the negation of a clause body with some local variable. Depending on the LP or CLP approach, universal quantification affects simple goals or constrained goals. In any case, universally quantified (constrained) goals are, in general, quite difficult to compute in an efficient manner. Besides, in [2] it is introduced the so-called negation technique and local variables absence is claimed as sufficient condition for the completeness of the technique. The negation technique is a fold/unfold transformation from normal logic programs into definite ones. The target program P0 contains a new predicates p0, for each predicate p in the source program P, such that the computation of a negative literal p(t) in P is simulated by the computation p0(t) in P0. In this paper, we introduce an effective transformation method that takes any definite logic program and yields an equivalent definite logic program without local variables. Source and target programs are equivalent w.r.t. threevalued logical consequences of program completion since, in further work, we plan to extend our results to normal logic programs. The underlying aim is to improve the performance of a practical implementation of constructive negation (cf. [1]). The transformation presented in this paper provides a way for efficient computation of negative queries w.r.t. a definite logic program. Efficiency is achieved because (1) the negative query is computed with respect to another definite logic program that has not local variables and (2) the target program comes from the compilation of the source program. In further work, we plan to extend our results to normal logic programs.

Palabras clave: program transformation, local variables, logic programming, negation.

Referencias:

[1] J. Álvez, P. Lucio, F. Orejas, E. Pasarella, and E. Pino. Constructive negation by bottomup computation of literal answers. In Applied Computing 2004, Proceedings of the 2004 ACM Symposium on Applied Computing, volume 2, pages 1468-1475. ACM Press, 2004.

[2] T. Sato and H. Tamaki. Transformational logic program synthesis. In Proceedings of International Conference on Fifth Generation Computer Systems, pages 195-201, 1984.

• Dealing denotationally with stream-based communication

Mercedes Hidalgo-Herrero y Yolanda Ortega Mallén

Categoría: 1 (Trabajo original)

Resumen:

Palabras clave: semánticas formales, semántica denotacional, programación funcional, paralelismo.

• A General Natural Rewriting Strategy

Santiago Escobar, José Meseguer y Prasanna Thati
(Universidad Politécnica de Valencia, U. Illinois at Urbana-Champaign - USA)

Categoría: 4 (Trabajo ya publicado - LOPSTR´04)

Resumen:
In [Escobar, Meseguer, Thati LOPSTR´04], we define an efficient rewriting strategy for general term rewriting systems. Several strategies have been proposed over the last two decades for rewriting, the most efficient of all being the \emph{natural rewriting strategy} of Escobar. All the strategies so far, including natural rewriting, assume that the given term rewriting system is left-linear and constructor-based. Although these restrictions are reasonable for some functional programming languages, they limit the expressive power of equational programming languages, and they preclude certain applications of rewriting to equational theorem proving and to languages combining equational and logic programming. We propose a conservative generalization of the natural rewriting strategy that does not require the previous assumptions for the rules and we establish its soundness and completeness.

Palabras clave: Demandedness, Rewriting Strategies, General Term Rewriting Systems.

• Invariant-based control of Maude execution: The LTL case

Francisco Durán y Manuel Roldán

Categoría: 1 (Trabajo original)

Resumen:
This work presents a general mechanism for executing specifications which comply with given invariants, which may be expressed in different formalisms. We exploit Maude´s reflective capabilities and its good properties as a semantic framework to provide a generic strategy that allows us to execute (possibly nonterminating and nonconfluent) Maude specifications taking into account the given invariants. Thus, the strategy is parameterized by the invariants and by the logic in which the invariants are expressed. Although other logics may be used, we focus in this work on the case of (Future Time) Linear Temporal Logic.

Palabras clave:

• Última actualización: 15/05/2008    Información de contacto: Salvador Lucas     Mantenimiento web: Raúl Fernández-Santa Cruz Jiménez

Incidencias inscripción: Carlos Canal