Verificación y Análisis
URI permanente para esta colección:
Artículos en la categoría Verificación y Análisis publicados en las Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo Testing of ATL programs from Randomly Generated Ecore Test ModelsAlmendros-Jiménez, Jesus M.; Becerra Terón, Antonio. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.Model transformation testing is crucial to detect incorrect transformations. Buggy transformations can lead to incorrect target models, either violating target meta-model requirements or more complex target model properties. In this paper we present a tool for testing ATL transformations. This tool is an extension of a previously developed tool for testing XML-based languages. With this aim an Ecore to XML Schema transformation is defined which makes to automatically generate random Ecore models possible. These randomly generated Ecore models are used to test ATL transformations. Properties to be tested are specified by OCL constraints, describing input and output conditions on source and target models, respectively.Artículo A tool for the automatic generation of logical models of order-sorted first-order theoriesGutiérrez, Raúl; Lucas, Salvador; Reinoso, Patricio. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.Semantics-based program analysis guarantees that the obtained knowledge about focused program features matches the real behaviour of the program. Automation of the analyses requires abstraction mechanisms to approximate the (usually undecidable) program semantics and targeted properties. In this setting, the logical notions of interpretation of a logic language and model of a theory provide an appropriate framework for abstraction in the sense that the corresponding analyses will be sound and, when relying on some decidable theory, amenable for automation. We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. Such theories are very helpful in the semantic description of most programming languages. The current version of the tool systematically exploits (and relies on) the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted convex matrix interpretations. The system is available as a web application and can be used to give support to users interested in checking properties of software modules provided that they are able to describe the property as an order-sorted first-order theory whose satisfiability guarantees the property. Examples of such properties are partial correctness, program termination, etc. The paper illustrates the use of the tool by means of simple case studies.Artículo How to construct a suite of program slicesInsa, David; Pérez Rubio, Sergio; Sílva, Josep. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.Program slicing is a technique to extract the part of a program (the slice) that influences or is influenced by a set of variables at a given point. Computing minimal slices is undecidable in the general case. Obtaining the minimal slice of a given program is computationally prohibitive even for very small programs. Hence, no matter what program slicer we use, in general, we cannot be sure that our slices are minimal. This is probably the fundamental reason why no benchmark collection of minimal program slices exists, even though this would be of great interest. In this work, we present the first suite of quasi-minimal slices (i.e., we cannot prove that they are minimal, but we provide technological evidences, based on different techniques, that they probably are). We explain the process of constructing the suite, the methodology and tools that were used, and the obtained results. The suite comes with a collection of Erlang benchmarks together with different slicing criteria and the associated quasi-minimal slices. This suite can be used to evaluate and compare program slicers, but it is particularly useful to develop slicers, because it contains scripts that allow for automatically validating a slicer against the whole suite. Concretely, these scripts produce reports about the impact on recall and precision of any change done during the development of the slicer.