George W. Ernst
Abstract
The programming language MODULA is extended to permit the formal specification of the structure and functional capabilities of modules. This makes true hierarchical programming possible in MODULA by allowing programmers of higher level parts of a system to ignore completely the internal structure of lower level modules and to rely entirely on the specifications of the capabilities of these modules. An example is included to illustrate this technique. We show that our specification mechanisms are sufficiently powerful to support formal verification rules for modules that have disjoint representations for abstract objects.
- 1 BARNARD, D.T., ELLIOT, W.D., AND THOMPSON, D.H. Euclid and Modula. SIGPLAN Notices (March 1978), 70-84.]] Google Scholar
- 2 BRADSHAW, F.T., AND ERNST, G.W. Formal specifications of a layer in a fde system. Rep. No. ESCI-79-1, Computer Engineering Dep., Case Western Reserve Univ., Cleveland, 1979.]]Google Scholar
- 3 CARTWRIaHT, R., AND OPPEN, D. Unrestricted procedure calls in Hoare's logic. In Proc. 5th ACM Principles of Programming Languages, 1978, pp. 131-140.]] Google Scholar
- 4 I)AHL, D.J., MYHRHAUG, B., AND NYGAARD, K. The Simula 67 Common Base Language. Norwegian Computing Center, Oslo, 1970.]]Google Scholar
- 5 DIJKSTRA, E. Notes on structured programming. In Structured Programming, O.J. Dahl et al., Eds., Academic Press, New York, 1972.]] Google Scholar
- 6 ERNST, G.W. Rules of inference for procedure calls. Acta Inf. (1977), 145-152.]]Google Scholar
- 7 FLON, L., AND MISRA, J. A unified approach to the specification and verification of abstract data types. In Proc. Specifications of Reliable Software Conf., IEEE Computer Society, 1979.]]Google Scholar
- 8 FLOYD, R.W. Assigning meanings to programs. In Proc. Applied Mathematics, Vol. 19, American Math. Society, Providence, R.I., 1967, pp. 19-32.]]Google Scholar
- 9 GRIE~, D., AND LEWN, G. A procedure call proof rule (with a simple explanation). Rep. TR79- 379, Dep. Computer Science, Cornel} Univ., Ithaca, N.Y., 1979.]]Google Scholar
- 10 HOARE, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), 576-582.]] Google Scholar
- 11 HOARE, C.A.R. Proof of correctness of data representations. Acta Inf. (1972), 271-281.]]Google Scholar
- 12 HOOKWAY, R.J. Verification of Data Abstractions whose Realization Shares Storage. Ph.D. dissertation, Computer Engineering and Science Dep., Case Western Reserve Univ., Cleveland, May 1980.]] Google Scholar
- 13 HOOKWAY, R.J., AND ERNST, G.W. A program verification system, in Proc. ACM Annual Conf., 1976.]] Google Scholar
- 14 JENSEN, K., AND W~RTH, N. Pascal User Manual and Report, Springer-Verlag, New York, 1976.]] Google Scholar
- 15 LAMPSON, B.W., HORNING, J.J., LONDON, R.L., MITCHELL, J.G., AND POPEK, G.J. Report on programming language Euclid. SIGPLAN Notices (Feb. 1977), 1-79.]] Google Scholar
- 16 LISKOV, B., SNYDER, A., ATKINSON, R., AND SCHAFFERT, C. Abstraction mechanisms in CLU. Comm. ACM 20, 10 (Aug. 1977), 564-577.]] Google Scholar
- 17 LONDON, R.L., GUTTAG, J.V., HORNING, J.J., LAMPSON, B.W., MITCHELL, J.G., AND POPEK, G.J. Proof rules for the programming language Euclid. Acta Inf. 10 (1978), 1-26.]]Google Scholar
- 18 NAVLAKHA, J.K. A syntax directed program verification system. Rep. No. ECIS-77-3, Computer Engineering Dep., Case Western Reserve Univ., Cleveland, Feb. 1978.]]Google Scholar
- 19 PARNAS, D.L. On the criteria to be used in decomposing systems into modules. Comm. ACM 17, 12 (Dec. 1972), 1053-1058.]] Google Scholar
- 20 STAY, J.F. HIPO and integrated program design. IBM Syst. J. 15, 2 (1976), 143-154.]]Google Scholar
- 21 WiR?H, N. Modula: A language for modular multiprogramming. Software--Practice and Experience (Jan. 1977), 3-35.]]Google Scholar
- 22 WULF, W.A., LONDON, R.L., AND SHAW, M. An introduction to the construction and verification of Alphard programs. IEEE Trans. Softw. Eng. (Dec. 1976), 253-264.]]Google Scholar
Index Terms
- Specification of Abstract Data Types in Modula
Recommendations
OBSCURE a specification language for abstract data types
OBSCURE is a specification language for abstract data types. It differs from classical specification languages by handling models rather than theories. The goal of the paper is to present a complete and precise description ofOBSCURE.
First, the different ...
Euclid and Modula
Both Euclid and Modula are programming languages based on Pascal and intended for writing system software such as operating system kernels. The further goals of each language, however, resulted in two rather different languages. Modula is meant to be ...
Programming with abstract data types
Proceedings of the ACM SIGPLAN symposium on Very high level languagesThe motivation behind the work in very-high-level languages is to ease the programming task by providing the programmer with a language containing primitives or abstractions suitable to his problem area. The programmer is then able to spend his effort ...
Comments