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

Hermenegildo, Manuel V.; Puebla Sánchez, Alvaro Germán y Bueno Carrillo, Francisco (1999). Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging. En: "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.

Descripción

Título: Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging
Autor/es:
  • Hermenegildo, Manuel V.
  • Puebla Sánchez, Alvaro Germán
  • Bueno Carrillo, Francisco
Editor/es:
  • Apt, Krzysztof R.
  • Marek, Victor W.
  • Truszczynski, Mirek
  • Warren, David S.
Tipo de Documento: Sección de Libro
Título del Libro: The Logic Programming Paradigm
Fecha: Julio 1999
ISBN: 9783642642494
Volumen: Part I
Materias:
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 14573
Identificador DC: http://oa.upm.es/14573/
Identificador OAI: oai:oa.upm.es:14573
Identificador DOI: 10.1007/978-3-642-60085-2_7
URL Oficial: http://link.springer.com/chapter/10.1007%2F978-3-642-60085-2_7
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 01 Mar 2013 08:01
Ultima Modificación: 21 Abr 2016 14:18
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM