Jornadas sobre Programación y Lenguajes (PROLE)

URI permantente para esta comunidad:

https://hdl.handle.net/11705/1865

Las Jornadas de PROgramación y LEnguajes (PROLE) constituyen un marco propicio de reunión, debate y divulgación para los grupos españoles que investigan en temas relacionados con la programación y los lenguajes de programación. Con la organización de este evento nacido en 2001, de carácter anual, se pretende fomentar el intercambio de experiencias y resultados, así como la comunicación y cooperación entre dichos grupos.

Examinar

Mostrando 1 - 20 de 191

Property based Testing of XQuery Programs
Almendros-Jiménez, Jesus M.; Becerra Terón, Antonio. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
In this paper we present the elements of an XQuery testing tool which makes possible to automatically test XQuery programs. The tool is able to systematically generate XML instances (i.e., test cases) from a given XML schema. The number and type of instances is defined by the human tester. These instances are used to execute the given XQuery program. In addition, the tool makes possible to provide an user defined property to be tested against the output of the XQuery program. The property can be specified with a Boolean XQuery function. The tool is implemented as an oracle able to report whether the XQuery program passes the test, that is, all the test cases satisfy the property, as well as the number of test cases used for testing. In the case when the XQuery program fails the testing, the tool shows counterexamples found in the test cases. The tool has been implemented as an XQuery library which makes possible to be used from any XQuery interpreter.
Learning a Subclass of Multivalued Dependencies Formulas from Entailments
Hermo, Montserrat; Ozaki, Ana. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Functional and multivalued dependencies play an important role in the design of relational databases. There is a strong connection between data dependencies and some fragments of the propositional logic. In particular, functional dependencies are closely related to Horn formulas. Also, multivalued dependencies are characterized in terms of multivalued formulas. It is known that both Horn formulas and sets of functional dependencies are efficiently learnable in the exact model of learning with queries. In this work, we study the learnability of a non-trivial subclass of multivalued formulas called CRMVDF. We use Angluin’s exact learning model with membership and equivalence queries and present a polynomial time algorithm which exactly learns CRMVDF from entailments.
Inferring Specifications in the K framework
Alpuente, María; Pardo, Daniel; Villanueva, Alicia. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this paper we propose a technique for automatically discovering specifications from real code. The proposed methodology relies on the symbolic execution capabilities recently provided by the K framework that we exploit to automatically infer formal specifications from programs that are written in a non–trivial fragment of C, called KERNELC. Roughly speaking, our symbolic analysis of KERNELC programs explains the execution of a (modifier) function by using other (observer) routines in the program. We implemented our technique in the automated tool KINDSPEC 2.0, which generates axioms that describe the precise input/output behavior of C routines that handle pointerbased structures (i.e., result values and state change). We describe the implementation of our system and discuss the differences w.r.t. our previous work on inferring specifications from C code.
A Declarative Debugger for Concurrent Erlang Programs
Caballero, Rafael; Martin-Martin, Enrique; Riesco, Adrián; Tamarit, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Erlang is a concurrent language with features such as actor model concurrency, no shared memory, message passing communication, high scalability and availability. However, the development of concurrent programs is a complex and error prone task. In this paper we present a declarative debugging approach for concurrent Erlang programs. Our debugger asks questions about the validity of transitions between the different points of the program that involve message passing and/or process creation. The answers, which represent the intended behavior of the program, are compared with the transitions obtained in an actual execution of the program. The differences allow us to detect program errors and to point out the pieces of source code responsible for the bugs. In order to represent the computations we present a semantic calculus for concurrent Core Erlang programs. The debugger uses the proof trees in this calculus as debugging trees used for selecting the questions asked to the user. The relation between the debugging trees and the semantic calculus allows us to establish the soundness of the approach. The theoretical ideas have been implemented in a debugger prototype.
Restricted Predicates for Hypothetical Datalog
Sáenz Pérez, Fernando. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Hypothetical Datalog is based on an intuitionistic semantics rather than on a classical logic semantics, and embedded implications are allowed in rule bodies. While the usual implication (i.e., the neck of a Horn clause) stands for inferring facts, an embedded implication plays the role of assuming its premise for deriving its consequence. A former work introduced both a formal framework and a goal-oriented tabled implementation, allowing negation in rule bodies. While in that work positive assumptions for both facts and rules can occur in the premise, negative assumptions are not allowed. In this work, we cover this subject by introducing a new concept: a restricted predicate, which allows negative assumptions by pruning the usual semantics of a predicate. This new setting has been implemented in the deductive system DES.
Prefacio
Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Prefacio de las XV Jornadas de Programación y Lenguajes (PROLE 2015).
Índice
Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Índice de las Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015).
Reasoning about policy behavior in logic-based trust management systems: Some complexity results and an operational framework
Pasarella, Edelmira; Lobo, Jorge. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
In this paper we show that the logical framework proposed by Becker et al. [1] to reason about security policy behavior in a trust management context can be captured by an operational framework that is based on the language proposed by Miller in 1989 to deal with scoping and/or modules in logic programming. The framework of Becker et al. uses propositional Horn clauses to represent both policies and credentials, implications in clauses are interpreted in counterfactual logic, a Hilbertstyle proof system is defined and a system based on SAT is used to prove whether properties about credentials, permissions and policies are valid, i.e. true under all possible policies. Our contributions in this paper are three. First, we show that this kind of validation can rely on an operational semantics (derivability relation) of a language very similar to Miller’s language, which is very close to derivability in logic programs. Second, we are able to establish that, as in propositional logic, validity of formulas is a co-NP-complete problem. And third, we present a provably correct implementation of a goal-oriented algorithm for validity.
Constraint Programming Meets SQL
Caballero, Rafael; Ieva, Carlo. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
We present a proposal for introducing SQL tuples into the modeling programming language MINIZINC. The domain of the new decision variables is defined by arbitrary relational database tables indicated by the user. The new setting increases the expressiveness of MINIZINC, allowing the modeler to mix the usual finite domains already existing in the language with string constraints typical from SQL such as concat, substr, or like. In order to obtain the solutions of these combined models, we first replace the atomic constraints involving strings by boolean variables. The result is a standard MINIZINC model, which can be solved by any off-the-shelf solver. Then, each individual solution is applied to the remainder string constraints, which are then solved using an SQL query. We discuss how both languages, MINIZINC and SQL, benefit from this combination.
An Assertional Proof of the Stability and Correctness of Natural Mergesort
Rustan M. Leino, K.; Lucio, Paqui. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Natural Mergesort [9] is a sorting algorithm for linear data structures (arrays and lists) that has been widely studied mainly due to its good properties. It has Nlog(N) worst-case complexity and, even in the case of arrays, is slightly easier to code than heapsort. Further, it performs very well on input data that is already mostly sorted. Another good property is stability. A sorting algorithm is stable if it maintains the relative order of records with equal keys. The most obvious application of a stable algorithm is sorting using different (primary, secondary, etc.) keys. Stability is, as we show in lemma EqMultisets, stronger than the property of preserving the multiset of elements (from the input list to the sorted output list). Hence, stability, along with sortedness, implies the correctness of sorting algorithms (including the permutation property). Recently, Sternagel [13] has published an Isabelle/HOL proof of the correctness and stability of natural mergesort as a proof pearl. Sternagel [13], firstly, specifies the algorithm as a functional program and, then, formalizes and proves the desired properties using the proof-assistant Isabelle/HOL. The proof is non-assertional and uses higher-order constructions. Indeed, it is strongly based on two skillful ad-hoc induction schemes. The first one for handling the mutually recursive functions involved in the splitting of the input into ascending sequences. The second induction scheme is related to the merging of the ascending lists. Correctness and stability are deduced from auxiliary lemmas which are proved by means of these induction schemes and with the help of a subtle generalization of the predicate sorted. The definition of that generalization and the induction schemes require the power of higher-order logic. In particular, the stability property is formalized in higher-order logic. More recently, de Gouw et al. [7] discussed a semi-automated formal proof of the correctness and stability of two sorting algorithms on arrays: Counting sort and Radix sort. This proof is formalized using the theorem-prover KeY [2]. The implementation code is written in Java. The specification is written (using the Java Modeling Language, JML) in an extension of first-order logic with permutation predicates, which have recently been added [1] to the KeY system. There are many other formalizations of the natural mergesort algorithm and also of different sorting algorithms (e.g. insertion sort, quicksort, heapsort, radix sort, etc.) in various systems, such as Coq [3], Isabelle/HOL [12], Why3 [6], ACL2 [8], KeY [2], etc. However, to the best of our knowledge, stability is only considered in [13], [7], and in our assertional proof. In this paper, we present an implementation of natural mergesort over an algebraic data type of lists. The code is enriched with its contract-based specification and a proof of its correctness and its stability. Our proof is assertional, i.e. it uses assert statements, inserted in the code, to enable the (fully) automatic verification. The assertions are first-order formulas that explain how and why the program works. The proof is supported by a few definitions that are easy to understand, and a few lemmas that isolate useful properties. Moreover, only non-trivial lemmas have detailed proofs and these are short and easy to read and to understand. Hence, in our opinion, the presented proof is quite clear and elegant. The program-proof is implemented in the state-of-the-art verifier Dafny [10]. The Dafny programming language supports a mixture of imperative, object-oriented programming and functional programming. In this paper, we use mostly functions, methods, and algebraic datatypes. The Dafny specification language includes the usual assertional language for contracts of pre/post conditions, invariants, decreasing expressions for termination proofs, etc. Since Dafny is designed with the main purpose of facilitating the construction of correct code, Dafny notation is compact and easy to understand. For the sake of readability and conciseness, the Dafny proof language includes constructs for structuring proofs such as lemmas and calculational proofs [11]. Dafny automatically generates executable .NET code for verified programs. The presented proof is made on the basis of some lemmas that ensure natural properties. Most of the proofs are inductive and use calculations [11] when appropriate. We believe that our program-proof is a simple and intuitive example of how a practical verification tool can be used by software developers with a minimum of familiarity with contract-based specifications and first-order assertions. We aim to contribute to the spread of the educational use of automatic tools in the development of formally verified software. We are convinced that this kind of example is useful for the introduction of formal software development methods and tools in software engineering courses. To sum up, we present a mechanically verified implementation of the sorting algorithm Natural Mergesort that consists of a few methods specified by their contracts of pre/post conditions. Methods are annotated with assertions that allow the automatic verification of the contract satisfaction. Along the paper we provide and explain the complete text of the program-proof.
A Generic Intermediate Representation for Verification Condition Generation, Work in Progress
Montenegro, Manuel; Peña Marí, Ricardo; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.
Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending Story
Romero-Hernández, David; de Frutos Escrig, David; Della Monica, Dario. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
We have developed a global approach to define bisimulation distances which goes somehow further away than the bisimulation distances based on the bisimulation game, previously proposed by some other authors. Our proposal is based on the cost of transformations: how much we need to modify one of the compared processes to obtain the other. Our original definition only covered finite processes, but a coinductive approach extends it to cover infinite but finitary trees. We have shown many interesting properties of our distances, and we wanted to prove their continuity with respect to projections, bur unfortunately we have not been able to accomplish that task. However, we have obtained several partial results that we now present in this paper.
Thresholded Debugging of XPath Queries
Almendros-Jiménez, Jesus M.; Luna, Alejandro; Moreno, Ginés. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
We have recently designed/implemented a method for debugging Fuzzy-XPath queries which produces a set of alternative Fuzzy-XPath expressions with higher chances for retrieving answers from XML files. The main goal of the present paper consists in the introduction of a new fuzzy command inside the Fuzzy-XPath debugger which comfortably relies on our implementation based on fuzzy logic programming. So, when <<[FILTER=r]>> precedes a fuzzy query the debugger lazily explores an input XML document for dynamically disregarding as soon as possible those branches of the XML tree leading to irrelevant solutions (i.e., with a chance degree degraded below r), thus allowing the possibility of efficiently managing large files without reducing the set of answers for which users are mainly interested in. Hence, advice that this dynamic thresholding technique embedded into the core of the Fuzzy-XPath debugger has two advantages: • firstly it permits to concentrate on significant answers (i.e., alternative queries which do not excessively deviate from the original one) without disturbing the attention with useless information, and • secondly, the computational behavior of the debugging process is highly improved (both in time and space) since a great amount of work is avoided when discriminating useless branches of the XML tree.
Towards a Formal Semantics-Based Technique for Interprocedural Slicing
Asavoae, Irina Mariuca; Asavoae, Mihail; Riesco, Adrián. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Interprocedural slicing is a technique applied on programs with procedures which relies on how the information is passed at procedure call/return sites. Such a technique computes program slices (i.e. program fragments restricted w.r.t. a given criterion). The existing approaches to interprocedural slicing exploit the particularities of the underlying language semantics in order to compute program slices. In this paper we propose a generic technique for interprocedural slicing. More specifically, our approach works with inferred particularities of a language semantics, given as a rewriting-logic specification, and computes program slices using a term slicing-based algorithm.
HR-SQL: An SQL Database System with Extended Recursion and Hypothetical Reasoning
Nieva, Susana; Sáenz Pérez, Fernando; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
In a former work we described the system and language R-SQL that overcomes some limitations of recursion of the relational database language SQL. Such limitations are non-linearity, mutual recursion, and some combinations of negation with recursion. In addition, R-SQL improved termination properties of recursive definitions. Next, this language was extended to include a restricted form of hypothetical relations and queries using assumptions, obtaining the language HR-SQL, and a preliminary implementation was developed for it. Here, we develop a new system HR-SQL from scratch and enhance the former system in several areas. First, hypothetical reasoning is fully integrated with recursive definitions. Second, the Python script generated by the system for computing the extension (materialization) of a database is now targeted to several state-of-the-art relational database systems. Third, the system has been interfaced to the integrated development environment ACIDE, allowing both a more friendly user interaction and a graphical view of the dependency graph that shows dependencies between relations. Fourth, being developed in Prolog, we have targeted it to both SICStus Prolog and SWI-Prolog, also providing standalone executables. Finally, the system has been extended with a bundle of commands, highly improving its capabilities with respect to the former system.
A Haskell Implementation of a Rule-Based Program Transformation for C Programs
Tamarit, Salvador; Vigueras, Guillermo; Carro, Manuel; Mariño, Julio. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Obtaining good performance when programming heterogeneous computing platforms poses significant challenges for the programmer. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code is transformed into a functionally equivalent one better suited for a given platform. The transformation rules are formalized in a domain-specific language (STML) that takes care of the syntactic and semantic conditions required to apply a given transformation. STML rules are compiled into Haskell function definitions that operate at AST level. Program properties, to be matched with rule conditions, can be automatically inferred or, alternatively, stated as annotations in the source code. Early experimental results are described.
A Declarative Semantics for a Fuzzy Logic Language Managing Similarities and Truth Degrees
Julián Iranzo, Pascual; Moreno, Ginés; Penabad, Jaime; Vázquez, Carlos. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
This work proposes a declarative semantics based on a fuzzy variant of the classical notion of least Herbrand model for the so-called FASILL language (acronym of “Fuzzy Aggregators and Similarity Into a Logic Language”) which has being recently designed and implemented in our research group for coping with implicit/explicit truth degree annotations, a great variety of connectives and unification by similarity.
A liberal type system for functional logic programs
López-Fraguas, Francisco J.; Martin-Martin, Enrique; Rodríguez-Hortalá, Juan. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
We propose a new type system for functional logic programming which is more liberal than the classical DamasMilner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from DamasMilner typing of expressions, we propose a new notion of well-typed program that adds support for type-indexed functions, a particular form of existential types, opaque higherorder patterns and generic functions as shown by an extensive collection of examples that illustrate the possibilities of our proposal. In the negative side, the types of functions must be declared, and therefore types are checked but not inferred. Another consequence is that parametricity is lost, although the impact of this flaw is limited as free theorems were already compromised in functional logic programming because of non-determinism.
Automatic generation of logical models for order-sorted first-order theories in program analysis
Lucas, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Computations are often viewed as proofs of specific sentences in some computational logic describing the operational semantics of the programming language or computational system. Since the semantics of programs (i.e., the set of such specific sentences that are provable in the logic) is usually incomputable, and most program properties undecidable, abstraction is essential in program analysis. Abstractions can be formalized as semantic models which should be automatically generated in a push-the-button-and-wait style of program analysis and verification. We investigate the automatic generation of numerical models for order-sorted first-order logics and its use in program analysis. Our development systematically uses the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of sorted signatures by means of appropriately adapted convex matrix interpretations. Such numerical interpretations permit the use of existing algorithms and tools from linear algebra (e.g., Farkas’ Lemma), real algebraic geometry, and arithmetic constraint solving in the implementation of the analyses.
A Collection of Website Benchmarks Labelled for Template Detection and Content Extraction
Alarte, Julián; Insa, David; Sílva, Josep; Tamarit, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Template detection and content extraction are two of the main areas of information retrieval applied to the Web. They perform different analyses over the structure and content of webpages to extract some part of the document. However, their objectives are different. While template detection identifies the template of a webpage (usually comparing with other webpages of the same website), content extraction identifies the main content of the webpage discarding the other part. Therefore, they are somehow complementary, because the main content is not part of the template. It has been measured that templates represent between 40% and 50% of data on the Web. Therefore, identifying templates is essential for indexing tasks because templates usually contain irrelevant information such as advertisements, menus and banners. Processing and storing this information is likely to lead to a waste of resources (storage space, bandwidth, etc.). Similarly, identifying the main content is essential for many information retrieval tasks. In this paper, we present a benchmark suite to test different approaches for template detection and content extraction. The suite is public, and it contains real heterogeneous webpages that have been labelled so that different techniques can be suitable (and automatically) compared.

Examinar

Examinando Jornadas sobre Programación y Lenguajes (PROLE) por Fecha de publicación

Resultados por página

Opciones de ordenación