| 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). |
|||
| 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:
|
||||