|Fulltext||PDF (requires Acrobat Reader)|
|Fulltext||PostScript (requires a PostScript Reader)|
|Article title:||A Floyd-Hoare Method for Prolog|
|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
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|
|No. of pages:||15|
|Series:||Linköping Electronic Articles in Computer and Information Science|
|REFERENCE TO THIS PAGE: