Proving deadlock freedom of logic programs with dynamic scheduling

In increasingly many logic programming systems, the Prolog left to right selection rule has been replaced with dynamic selection rules, that select an atom of a query among those satisfying suitable conditions. These conditions describe the form of the arguments of every program predicate, by means of a so-called delay declaration. Dynamic selection rules introduce the possibility of deadlock, an abnormal form of termination that occurs if the query is non-empty and it contains no `selectable' atoms. In this paper, we introduce a simple compositional assertional method for proving deadlock freedom. The method is based on the notion of suspension cover, a static description of the possible dynamic schedulings of the body atoms of a clause, according to a given delay declaration. In the method, we assume that monotonic assertions are used for specifying the conditions of the delay declaration. Apart sections are devoted to two more practical instances of the method, that use types and modes, respectively.