IDA Dept. of Computer and Information science, Linköping University

IDA Technical Reports: abstract

Generated: Sun, 23 Apr 2017 15:52:23

Drabent, W. and Maluszynski, J. (1986). Proving Run-Time Properties of Logic Programs. Technical Report LiTH-IDA-R-86-23, Department of Computer and Information Science, Linköping University, Sweden. (bibtex),

Abstract: Certain properties of logic programs are inexpressible in terms of their declarative semantics. One example of such properties would be the actual form of procedure calls and successes which occur during computations of a program. They are often used by programmers in their informal reasoning. In this paper, the inductive assertion method for proving partial correctness of logic programs is introduced and proved sound. The method makes it possible to formulate and prove properties which are inexpressible in terms of the declarative semantics. An execution mechanism using the Prolog computation rule and arbitrary search strategy (eg. OR-parallelism or Prolog backtracking) is assumed. The method may be also used to specify the semantics of some extra-logical built-in procedures for which the declarative semantics is not applicable.

Goto (at Linköping University): CS Dept TR Overview