Steadfast Logic Programs

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom.
kung-kiu@cs.man.ac.uk  

Mario Ornaghi
Dipartimento di Scienze dell'Informazione
Universita' degli studi di Milano
Via Comelico 39/41, 20135 Milano, Italy.
ornaghi@dsi.unimi.it 

Sten-Ake Tarnlund
Computing Science Department, Uppsala University
P.O. Box 520, S-751 20 Uppsala, Sweden.
stenake@csd.uu.se

Abstract:
We present the notion of steadfastness that at once embodies modularity, 
reusability, and formal correctness. A steadfast program is an open program 
with parameters, which is parametrically correct in the sense that it will 
always be correct wrt its (open) specification whenever its parameters are
computed correctly. Thus, a steadfast program is correct, modular and reusable. 
Therefore, steadfastness provides a basis for hierarchical construction of
correct reusable modules. We first introduce the idea of steadfastness
in an informal manner. Then we give a model-theoretic characterisation
of steadfastness, followed by an operational semantics based on the (open) 
completion of an open program. Finally, we apply our general results to 
program correctness with respect to parametric specifications.