Responsible for this page: David Lawrence, davla@ep.liu.se
Page last updated: 2008-07-17
|
Content
| Files: | Description | File size | Format | |
| Fulltext | 246K | PDF (requires Acrobat Reader) | ||
| Fulltext | 216K | 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 | |||
| Checksum PDF: | 47dddef326c69103d85fef859be6d41f /home/ep/www/ea/cis/1997/013/cis97013.pdf (MD5) | |||
| Checksum PS: | 9cbbafe8a6686a702ae339f5f7b9094c /service/www-ep/docs/ea/cis/1997/013/cis97013.ps (MD5) | |||
| PGP PDF: | PGP | |||
| PGP PS: | PGP | |||
| Old Checksum: | Checksum (PS) | Information about recalculation of Checksum | |||
| SPECIAL INFO: | Checksum, PGP and persistence | |||
REFERENCE TO THIS PAGE:
|
||||
Last updated: 2008-07-17