Type Analysis for CHIP

Abstract. This paper proposes a tool to support reasoning about (partial) correctness of constraint logic programs. The tool infers a speci cation that approximates the semantics of a given program. The semantics of interest is an operational \call-success" semantics. The main intended application is program debugging. We consider a restricted class of speci cations, which are regular types of constrained atoms. Our type inference approach is based on bottom-up abstract interpretation, which is used to approximate the declarative semantics (c-semantics). By using \magic transformations" we can describe the call-success semantics of a program by the declarative semantics of another program. We are focused on CLP over nite domains. Our prototype program analyzer works for the programming language CHIP.

• Type: Conference
• Year: 1998
• Where: AMAST
• Authors: Wlodzimierz Drabent, Pawel Pietrzak
• Keywords: AMAST 1998, Declarative Semantics, Semantics, Software Engineering, Speci Cations