Modules, Reuse and Correctness 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 Abstract: Modules are essential for systematic software development. For formal software development, where (formal) correctness is paramount, modules should have suitable forms and a formal semantics for (reasoning about) their correctness and reuse. In this paper, we define modules as first-order theories (with isoinitial semantics) that contain logic programs, and define and discuss such modules, their reuse and composition, and their correctness. We show that our approach provides a logical basis for formal program development in an object-oriented fashion.