Reasoning about Prolog programs: From modes through types to assertions

1 November 1994

journal article
research article
Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing

Vol. 6 (Suppl 1) , 743-765
https://doi.org/10.1007/bf01213601

Abstract

We provide here a systematic comparative study of the relative strength and expressive power of a number of methods for program analysis of Prolog. Among others we show that these methods can be arranged in the following hierarchy: mode analysis ⇒ type analysis ⇒ monotonic properties ⇒ nonmonotonic run-time properties. We also discuss a method allowing us to prove global run-time properties.

Keywords

This publication has 7 references indexed in Scilit:

On the occur-check-free PROLOG programs
ACM Transactions on Programming Languages and Systems, 1994
Proving termination of logic programs by exploiting term properties
Published by Springer Nature ,1991
Logic Programming
Published by Elsevier ,1990
Verifying correctness of logic programs
Published by Springer Nature ,1989
Inductive assertion method for logic programs
Theoretical Computer Science, 1988
Foundations of Logic Programming
Published by Springer Nature ,1987
The relation between logic and functional languages: a survey
The Journal of Logic Programming, 1986