Files: Description File size 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).
PDF
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
REFERENCE TO THIS PAGE:
Drabent, Wlodzimierz (1997). A Floyd-Hoare Method for Prolog in Linköping Electronic Articles in Computer and Information Science, Vol. 2. http://www.ep.liu.se/ea/cis/1997/013/. ()