An integrated approach to assertion-based random testing in Prolog

Casso, Ignacio de and Morales Caballero, José Francisco and López García, Pedro and Hermenegildo, Manuel V. (2019). An integrated approach to assertion-based random testing in Prolog. In: "29th International Symposium on Logic-Based Program Synthesis and Transformation ( LOPSTR 2019)", 8-10 Oct 2019, Oporto, Portugal. ISBN 978-3-030-45259-9. pp. 159-176. https://doi.org/10.1007/978-3-030-45260-5_10.

Description

Title: An integrated approach to assertion-based random testing in Prolog
Author/s:
  • Casso, Ignacio de
  • Morales Caballero, José Francisco
  • López García, Pedro
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 29th International Symposium on Logic-Based Program Synthesis and Transformation ( LOPSTR 2019)
Event Dates: 8-10 Oct 2019
Event Location: Oporto, Portugal
Title of Book: Logic-Based Program Synthesis and Transformation
Date: 2019
ISBN: 978-3-030-45259-9
Volume: 12042
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

We present an approach for assertion-based random testing of Prolog programs that is tightly integrated within an overall assertionbased program development scheme. Our starting point is the Ciao model, a framework that unifies unit testing and run-time verification, as well as static verification and static debugging, using a common assertion language. Properties which cannot be verified statically are checked dynamically. In this context, the idea of generating random test values from assertion preconditions emerges naturally since these preconditions are conjunctions of literals, and the corresponding predicates can in principle be used as generators. Our tool generates valid inputs from the properties that appear in the assertions shared with other parts of the model, and the run time-check instrumentation of the Ciao framework is used to perform a wide variety of checks. This integration also facilitates the combination with static analysis. The generation process is based on running standard predicates under non-standard (random) search rules. Generation can be fully automatic but can also be guided or defined specifically by the user. We propose methods for supporting (C)LP-specific properties, including combinations of shape-based (regular) types and variable sharing and instantiation, and we also provide some ideas for shrinking for these properties. We also provide a case study applying the tool to the verification and checking of the code of some of the abstract domains used by the Ciao system.

Funding Projects

TypeCodeAcronymLeaderTitle
Government of SpainTIN2015-67522-C3-1-RTRACESFundación IMDEA SoftwareTecnologías y herramientas para el desarrollo de software consciente de los recursos, correcto y eficiente (IMDEA)
Madrid Regional GovernmentP2018/TCS-4339BLOQUES-CMUnspecifiedContratos inteligentes y blockchains escalables y seguros mediante verificación y análisis

More information

Item ID: 62526
DC Identifier: http://oa.upm.es/62526/
OAI Identifier: oai:oa.upm.es:62526
DOI: 10.1007/978-3-030-45260-5_10
Official URL: https://link.springer.com/content/pdf/10.1007%2F978-3-030-45260-5_10.pdf
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 01 May 2020 07:52
Last Modified: 01 May 2020 07:52
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM