Inferring call and success types for CLP programs
1998 (English)Other (Refereed)
This paper proposes a tool to support reasoning about (partial) correctness of constraint logic programs. The tool infers a specification that approximates the semantics of a given program. The main intended application is program debugging. We deal with a "callsuccess "semantics of CLP. We consider a restricted class of specifications, which are regular types of constrained atoms. The call-success semantics of a CLP program is characterized by the declarative semantics of another CLP program ("magic transformation"). Then bottom-up abstract interpretation is used to approximate the latter. We study the theoretical background of this approach.
We are mainly interested in applying it to CLP over finite domains. Our prototype program analyzer works for the programming language CHIP. 1 Introduction and motivation The work reported addresses the problem of correctness of CLP programs. Intuitively, a program is correct if it behaves as expected by the user. But user expectations are seldo.
Place, publisher, year, edition, pages
Engineering and Technology
IdentifiersURN: urn:nbn:se:liu:diva-87992OAI: oai:DiVA.org:liu-87992DiVA: diva2:600985
EPSRIT DiSCiPl deliverable, September 19982013-01-282013-01-282013-01-31Bibliographically approved