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 semantics, and contrasts this with the Alphard formalism based on Hoare logic.
Research of Drs. Gannon and Hamlet was partially supported by the Air Force Office of Scientific Research under contract F49620-80-C-0004.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
O.-J. Dahl, B. Myhrhaug, and K. Nygaard, The SIMULA 67 common base language. Norwegian Computing Center, Oslo, Publication Nr. S-22, 1970.
C. A. R. Hoare, Proof of correctness of data representations, Acta Informatica 1 (1972), pp. 271–281.
W. A. Wulf, R. L. London, and M. Shaw, An introduction to the construction and verification of Alphard programs, IEEE Trans. Software Engineering SE-2 (1976), pp. 253–265.
J. Guttag and J. Horning, The algebraic specification of abstract data types, Acta Informatica 10 (1978), 27–52.
J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright, Initial algebra semantics and continuous algebras, J. of the Assoc. for Comp. Mach. 24 (1977), pp. 68–95.
R. G. Hamlet and H. D. Mills, Functional semantics, University of Maryland Computer Science Technical Report 1238, 1983.
Ibid., Functional Analysis of Programs, Oregon Graduate Center Technical Report CS/E 84-006, October, 1984.
Linger, R.C., Mills, H.D., and Witt, B.I., Structured Programming: Theory and Practice, Addison-Wesley, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gannon, J., Hamlet, R., Mills, H. (1985). Functional semantics of modules. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds) Formal Methods and Software Development. TAPSOFT 1985. Lecture Notes in Computer Science, vol 186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15199-0_4
Download citation
DOI: https://doi.org/10.1007/3-540-15199-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15199-9
Online ISBN: 978-3-540-39307-8
eBook Packages: Springer Book Archive