ArtículoType Checking and Testing of SPARQL QueriesAlmendros-Jiménez, Jesus M.; Becerra Terón, Antonio. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.In this paper we describe a property-based testing tool for SPARQL. The tool randomly generates test cases in the form of instances of an ontology. The tool checks the well typed-ness of the SPARQL query as well as the consistency of the test cases with the ontology axioms. With this aim, a type system has been defined for SPARQL. Test cases are after used to execute queries. The output of the queries are tested with a Boolean property which is defined in terms of membership of ontology individuals to classes. The testing tool reports counterexamples when the Boolean property is not satisfied. ResumenTowards a formal framework for analyzing stream processing systems in MaudeRiesco, Adrián; Palomino, Miguel; Martí-Oliet, Narciso. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.With the rise of Big Data technologies, distributed stream processing systems (SPS) have gained popularity in the last years. Among these systems Spark Streaming stands out as a particularly attractive option, with a growing adoption in the industry, so we will consider in particular some features of SPS in Spark Streaming. Maude is a high-performance logical framework where other systems can be easily specified and executed. In this paper we show how a Maude specification of Spark Streaming would allow developers to analyze and prove properties on their programs. ResumenA Tool for Black-Box Testing in a Multilanguage Verification PlatformAracil, Marta; García, Pedro; Peña Marí, Ricardo. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.In the context of the multilanguage verification platform CAVI-ART, we have defined an Intermediate Representation (IR) to which all the source languages are translated. This IR contains both the code and the assertions given by the programmer. Its primary purpose was automatically generating and proving, in a source language independent way, the verification conditions ensuring the program correctness. The logical formulas are sent by the platform to an SMT solver which checks their validity. In this paper we present a new use of the IR: we transform it into an executable language (that it turns out to be Haskell) and also transform the assertions into executable (Haskell) code. Thanks to that, tests can be run on the transformed program, and bugs can be detected either in the specification assertions or in the code. Moreover, we use the assertions to generate black-box test-cases from them, and also as test oracles. In this way, given the IR of a program, all the process ---namely, test-case generation, test running, and test correctness checking--- is completely automatic. So, thousands of tests can be run with little or none effort. The only burden for the programmer is providing the precondition and the postcondition of the code under test, which anyway should have been provided in advance, since the primary goal was to verify the program. We discuss the problems we have encountered while implementing this idea, and how we have solved them. In particular, we report on the use of Haskell resources such as GADTs, efficient data structures, and specialized libraries.