Formal Reasoning about Modules, Reuse, and their Correctness

. We present a formalisation of modules that are correct , and (correctly) reusable in the sense that composition of modules preserves both correctness and reusability. We also introduce a calculus for formally reasoning about the construction of such modules. 1 Introduction Modular programming has been around for a long time, and has more recently evolved into object-oriented programming (e.g. [11]). Various forms of modules and objects can be found in a variety of modern programming languages. They are important because they facilitate structured design as well as code reuse. However, for formal program development, i.e. developing programs that are formally correct wrt their (formal) specifications, current modular and objectoriented programming languages lack a suitable formal semantics in our view, even though some of them do have type-system based rules for program composition (see e.g. [3, 13]). In this paper, we define modules as first-order theories (with isoinitial seman..