|
CS Seminar: Patricia M. Hill, January 26, 2000
- Speaker
-
Dr. Patricia M. Hill,
School of Computer Studies,
University of Leeds, UK.
- Date and Time
-
Wednesday, January 26, 2000 at 10:30
- Place
-
Sala Riunioni,
Dipartimento di Matematica,
Università di Parma,
Via D'Azeglio 85/A,
I-43100 Parma
- Title
-
Verification of Logic Programs with Delay Declarations
- Abstract
-
Program verification has to exploit a knowledge of the program
behaviour to ensure that the program executes terminates normally with
correct answers.
Prolog, although based on first order logic and has an implementation
based on resolution, has a number of practical features that may cause
a program to terminate abnormally. Moreover, most Prolog systems have
some form of delay declarations (eg the Block declarations of SICStus
Prolog) that allow the programmer to insist that certain atomic calls
are delayed until they are sufficiently instantiated.
We have considered a number of aspects of verification relevant to
Prolog programs. These include occur-check freedom, flounder freedom,
freedom from errors related to built-ins, and termination. The
occur-check in unification procedures which avoids the generation of
infinite data-structures is expensive and often omitted. Floundering
means that the program stops without any useful solution and is caused
when all the atoms to be executed are postponed because of the delay
declarations. Arithmetic operators provided in Prolog often require
the arguments to be ground and if they are not sufficiently
instantiated, the program terminates with an error message.
In this talk, I will describe existing techniques for verifying Prolog
programs without delay declarations and then show how this work can be
lifted to programs with delays such as the Block declarations of
SICStus Prolog.
- Contact Person
-
Roberto Bagnara
[Page last updated on February 22, 2002, 15:16:33.]
|