Formal Reasoning about Modules, Reuse and their Correctness

Christoph Kreitz
Fachgebiet Intellektik, Fachbereich Informatik
Technische Hochschule Darmstadt
Alexanderstr. 10, D-64283 Darmstadt, Germany
kreitz@intellektik.informatik.th-darmstadt.de

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

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

Abstract:
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.