article

Open access

Specification of Abstract Data Types in Modula

Editor: Susan L. Graham Authors:

George W. Ernst,

William F. OgdenAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 2, Issue 4

Pages 522 - 543

https://doi.org/10.1145/357114.357117

Published: 01 October 1980 Publication History

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.

References

[1]

BARNARD, D.T., ELLIOT, W.D., AND THOMPSON, D.H. Euclid and Modula. SIGPLAN Notices (March 1978), 70-84.]]

[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.]]

[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.]]

[4]

I)AHL, D.J., MYHRHAUG, B., AND NYGAARD, K. The Simula 67 Common Base Language. Norwegian Computing Center, Oslo, 1970.]]

[5]

DIJKSTRA, E. Notes on structured programming. In Structured Programming, O.J. Dahl et al., Eds., Academic Press, New York, 1972.]]

[6]

ERNST, G.W. Rules of inference for procedure calls. Acta Inf. (1977), 145-152.]]

[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.]]

[8]

FLOYD, R.W. Assigning meanings to programs. In Proc. Applied Mathematics, Vol. 19, American Math. Society, Providence, R.I., 1967, pp. 19-32.]]

[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.]]

[10]

HOARE, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), 576-582.]]

[11]

HOARE, C.A.R. Proof of correctness of data representations. Acta Inf. (1972), 271-281.]]

[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.]]

[13]

HOOKWAY, R.J., AND ERNST, G.W. A program verification system, in Proc. ACM Annual Conf., 1976.]]

[14]

JENSEN, K., AND W~RTH, N. Pascal User Manual and Report, Springer-Verlag, New York, 1976.]]

[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.]]

[16]

LISKOV, B., SNYDER, A., ATKINSON, R., AND SCHAFFERT, C. Abstraction mechanisms in CLU. Comm. ACM 20, 10 (Aug. 1977), 564-577.]]

[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.]]

[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.]]

[19]

PARNAS, D.L. On the criteria to be used in decomposing systems into modules. Comm. ACM 17, 12 (Dec. 1972), 1053-1058.]]

[20]

STAY, J.F. HIPO and integrated program design. IBM Syst. J. 15, 2 (1976), 143-154.]]

[21]

WiR?H, N. Modula: A language for modular multiprogramming. Software--Practice and Experience (Jan. 1977), 3-35.]]

[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.]]

Cited By

Bansal KKoskinen ETripp O(2020)Synthesizing Precise and Useful Commutativity ConditionsJournal of Automated Reasoning10.1007/s10817-020-09573-w64:7(1333-1359)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10817-020-09573-w
Bansal KKoskinen ETripp O(2018)Automatic Generation of Precise and Useful Commutativity ConditionsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_7(115-132)Online publication date: 12-Apr-2018
https://doi.org/10.1007/978-3-319-89960-2_7
Pike SHeym WAdcock BBronish DKirschenbaum JWeide BArora SBruegge BLeavens GCoady YPeyton-Jones S(2009)Traditional assignment considered harmfulProceedings of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications10.1145/1639950.1640056(909-916)Online publication date: 25-Oct-2009
https://dl.acm.org/doi/10.1145/1639950.1640056
Show More Cited By

Index Terms

Specification of Abstract Data Types in Modula
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types
      2. Language types

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 languages

The 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 2, Issue 4

Oct. 1980

131 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/357114

Editor:
Susan L. Graham

Issue’s Table of Contents

Copyright © 1980 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 1980

Published in TOPLAS Volume 2, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
356
Total Downloads

Downloads (Last 12 months)52
Downloads (Last 6 weeks)10

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bansal KKoskinen ETripp O(2020)Synthesizing Precise and Useful Commutativity ConditionsJournal of Automated Reasoning10.1007/s10817-020-09573-w64:7(1333-1359)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10817-020-09573-w
Bansal KKoskinen ETripp O(2018)Automatic Generation of Precise and Useful Commutativity ConditionsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_7(115-132)Online publication date: 12-Apr-2018
https://doi.org/10.1007/978-3-319-89960-2_7
Pike SHeym WAdcock BBronish DKirschenbaum JWeide BArora SBruegge BLeavens GCoady YPeyton-Jones S(2009)Traditional assignment considered harmfulProceedings of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications10.1145/1639950.1640056(909-916)Online publication date: 25-Oct-2009
https://dl.acm.org/doi/10.1145/1639950.1640056
Tiuryn J(2005)A simple programming language with data types: semantics and verificationLogics of Programs10.1007/3-540-15648-8_29(387-405)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-15648-8_29
Ernst GHookway ROgden W(1994)Modular Verification of Data Abstractions with Shared RealizationsIEEE Transactions on Software Engineering10.1109/32.27757620:4(288-307)Online publication date: 1-Apr-1994
https://dl.acm.org/doi/10.1109/32.277576
Ernst GHookway RMenegay JOgden W(1991)Modular verification of Ada genericsComputer Languages10.1016/0096-0551(91)90010-716:3-4(259-280)Online publication date: 1-Apr-1991
https://dl.acm.org/doi/10.1016/0096-0551%2891%2990010-7
Hookway R(1985)Verifying Ada programsACM SIGSOFT Software Engineering Notes10.1145/1012497.101251510:4(51-52)Online publication date: 1-Aug-1985
https://dl.acm.org/doi/10.1145/1012497.1012515
Claybrook B(1983)Defining database views as data abstractions in EXT_ PascalInformation Systems10.1016/0306-4379(83)90003-08:3(165-176)Online publication date: Jan-1983
https://doi.org/10.1016/0306-4379(83)90003-0
Bradshaw FErnst GHookway R(1982)Use of data abstraction in process specificationACM SIGSOFT Software Engineering Notes10.1145/1010904.10109087:3(16-21)Online publication date: 1-Jul-1982
https://dl.acm.org/doi/10.1145/1010904.1010908

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents