Göm menyn
Files: Description Format
Fulltext PDF (requires Acrobat Reader)
Fulltext PostScript (requires a PostScript Reader)
Author: Wlodzimierz Drabent
Article title: A Floyd-Hoare Method for Prolog
Publ. type: Article
Volume: 2
Article No: 13
Language: English
Abstract [en]: We present an inductive assertion method for proving run-time properties of logic programs. The method could be seen as a logic programming counterpart of the well-known approach of Floyd and Hoare for imperative programs.
   The method concerns assertions assigned to program points and makes it possible to prove that whenever the control reaches a program point the corresponding assertion is satisfied.
   We also show a way of augmenting the method to prove termination. An assertion (assigned to a point in a program clause) describes a set of substitutions (for the variables of the clause).
   Assertions may be not monotonic (i.e. not closed under substitutions).
Publisher: Linköping University Electronic Press
Year: 1997
Available: 1997-12-19
No. of pages: 15
Series: Linköping Electronic Articles in Computer and Information Science
ISSN: 1401-9841

Responsible for this page: Peter Berkesand
Last updated: 2017-02-21