eprintid: 14573
rev_number: 19
eprint_status: archive
userid: 2047
dir: disk0/00/01/45/73
datestamp: 2013-03-01 08:01:07
lastmod: 2023-02-27 11:42:24
status_changed: 2023-02-27 11:42:24
type: book_section
metadata_visibility: show
item_issues_count: 0
creators_name: Hermenegildo, Manuel V.
creators_name: Puebla Sánchez, Alvaro Germán
creators_name: Bueno Carrillo, Francisco
title: Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging
ispublished: pub
subjects: informatica
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.
date: 1999-07
date_type: published
publisher: Springer Berlin Heidelberg
official_url: http://link.springer.com/chapter/10.1007%2F978-3-642-60085-2_7
id_number: 10.1007/978-3-642-60085-2_7
full_text_status: public
series: Artificial Intelligence
volume: Part I
pagerange: 161-192
pages: 456
institution: Informatica
department: Inteligencia_Artificial
refereed: TRUE
isbn: 9783642642494
book_title: The Logic Programming Paradigm
editors_name: Apt, Krzysztof R.
editors_name: Marek, Victor W.
editors_name: Truszczynski, Mirek
editors_name: Warren, David S.
rights: by-nc-nd
citation:   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 <https://doi.org/10.1007/978-3-642-60085-2_7>. 
document_url: https://oa.upm.es/14573/1/HERME_ARTINBOOKS_1999-1.pdf