|Publication Type||Journal Article|
|Year of Publication||1997|
|Authors||Zaffanella E, Giacobazzi R, Levi G|
|Journal||Journal of Functional and Logic Programming|
|Keywords||abstract interpretation, concurrent constraint programming, constraint systems, software verification, static analysis|
Because of synchronization based on blocking ask, some of the most important techniques for data-flow analysis of (sequential) constraint logic programs (clp) are no longer applicable to cc languages. In particular, the generalized approach to the semantics, intended to factorize the (standard) semantics so as to make explicit the domain-dependent features (i.e., operators and semantic objects that may be influenced by abstraction) becomes useless for relevant applications. In the case of clp programs, abstract interpretation of a program P is obtained by evaluating an abstract program α(P) into an instance of clp itself, provided with a suitable abstract constraint system. In cc programs, a correct characterization of suspended computations can only be obtained by replacing ask constraints with stronger constraints, which is not the case in abstract interpretation, where abstraction is usually a weakening of constraints. A possible solution to this problem is based on a more abstract (nonstandard) semantics: the success semantics, which models nonsuspended computations only. With a program transformation (NoSynch) that simply ignores synchronization, we obtain a clp-like program that allows us to apply standard techniques for data-flow analysis. For suspension-free programs, the success semantics is equivalent to the standard semantics, thus justifying the use of suspension analysis to generate sound approximations. A second transformation (Angel) is introduced, applying a different abstraction of synchronization in possibly suspending programs. The resulting abstraction is adequate to suspension analysis. Applicability and accuracy of these solutions are investigated.