Theory of Modules

1 July 1987

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering

Vol. SE-13 (7) , 820-829
https://doi.org/10.1109/tse.1987.233493

Abstract

Because large-scale software development is a struggle against internal program complexity, the modules into which programs are divided play a central role in software engineering. A module encapsulating a data type allows the programmer to ignore both the details of its operations, and of its value representations. It is a primary strength of program proving that as modules divide a program, making it easier to understand, so do they divide its proof. Each module can be verified in isolation, then its internal details ignored in a proof of its use. This paper describes proofs of module abstractions based on functional semantics, and contrasts this with the Alphard formalism based on Hoare logic.

Keywords

This publication has 0 references indexed in Scilit: