Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging

Hermenegildo, Manuel V. and Puebla Sánchez, Alvaro Germán and Bueno Carrillo, Francisco (1999). Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging. In: "The Logic Programming Paradigm". Artificial Intelligence, Part I . Springer Berlin Heidelberg, pp. 161-192. ISBN 9783642642494. https://doi.org/10.1007/978-3-642-60085-2_7.

Description

Title: Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging
Author/s:
  • Hermenegildo, Manuel V.
  • Puebla Sánchez, Alvaro Germán
  • Bueno Carrillo, Francisco
Editor/s:
  • Apt, Krzysztof R.
  • Marek, Victor W.
  • Truszczynski, Mirek
  • Warren, David S.
Item Type: Book Section
Title of Book: The Logic Programming Paradigm
Date: July 1999
ISBN: 9783642642494
Volume: Part I
Subjects:
Faculty: Facultad de Informática (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 discuss a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from (global) static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be checked statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by user programs. We also report briefly on an implementation of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis.

More information

Item ID: 14573
DC Identifier: http://oa.upm.es/14573/
OAI Identifier: oai:oa.upm.es:14573
DOI: 10.1007/978-3-642-60085-2_7
Official URL: http://link.springer.com/chapter/10.1007%2F978-3-642-60085-2_7
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 01 Mar 2013 08:01
Last Modified: 21 Apr 2016 14:18
  • 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