Smaus, J.G. and Hill, P.M. and King, A. (1998) Preventing Instantiation Errors and Loops for Logic Programs with Several Modes Using t block Declarations. University of Kent, University of Kent, Canterbury.
We present verification methods for logic programs with delay declarations, showing how type and instantiation errors related to built-ins can be avoided, and how termination can be ensured. Three features are distinctive of this work: (a) we assume that predicates can be used in several modes; (b) we show that block declarations, which are a particularly simple delay construct, are sufficient to ensure the desired properties; (c) we take the selection rule into account, assuming it to be the rule of most Prolog implementations. These methods can be used both to verify existing programs and to assist in writing new programs.
|Additional information:||Extended abstract. Accepted for presentation at the LOPSTR 98 workshop.|
|Uncontrolled keywords:||Logic programing, delay declaration, block declaration, built-in, error, termination, mode|
|Subjects:||Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,|
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group|
|Depositing User:||Mark Wheadon|
|Date Deposited:||07 Dec 2009 15:00|
|Last Modified:||25 Jun 2012 10:14|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/21649 (The current URI for this page, for reference purposes)|
- Depositors only (login required):