Functional Semantics of Modules.
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 the functional method of Mills, and contrasts this with the Alphard formalism based on Hoare logic. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1984
- Accession Number
- ADA146923
Entities
People
- D. Hamlet
- H. Mills
- J. Gannon
Organizations
- University of Maryland