Program verification and Prolog
Krzysztof Rafal Apt · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1995
We show here that verification of Prolog programs can be systematically carried out within a simple framework which comprises syntactic analysis, declarative semantics, modes and types. We apply these techniques to study termination, partial correctness, occurcheck freedom, absence of errors and absence of floundering. Finally, we discuss which aspects of these techniques can be automated. Notes. This research was partly supported by the ESPRIT Basic Research Action 6810 (Compulog 2). A preliminary, shorter, version of this paper appeared as Apt [3]. 1 Introduction 1.1 Motivation Prolog is 20 years old and so is logic programming. However, they were developed separately and these two developments never really merged. The first track is best exemplified by Sterling and Shapiro [36], which puts emphasis on programming style and techniques, and the second by Lloyd [25], which concentrates on the theoretical foundations. As a result of these separate developments, until recently little...