Verification of Logic Programs with Delay Declarations

. Logic programs augmented with delay declarations form a higly expressive programming language in which dynamic networks of processes that communicate asynchronously by means of multiparty channels can be easily created. In this paper we study correctness these programs. In particular, we propose proof methods allowing us to deal with occur check freedom, absence of deadlock, absence of errors in presence of arithmetic relations, and termination. These methods turn out to be simple modifications of the corresponding methods dealing with Prolog programs. This allows us to derive correct delay declarations by analyzing Prolog programs. Finally, we point out difficulties concerning proofs of termination. Note. The research of the first author was partly supported by the ESPRIT Basic Research Action 6810 (Compulog 2). 1 Introduction In Kowalski [Kow79] the slogan "Algorithm = Logic + Control" was coined. This paper suggested logic programming as a formalism for a systematic development ..