article

Free access

An example of hierarchical design and proof

Authors:

Jay M. Spitzen,

Karl N. Levitt,

Lawrence RobinsonAuthors Info & Claims

Communications of the ACM, Volume 21, Issue 12

Pages 1064 - 1075

https://doi.org/10.1145/359657.359667

Published: 01 December 1978 Publication History

Abstract

Hierarchical programming is being increasingly recognized as helpful in the construction of large programs. Users of hierarchical techniques claim or predict substantial increases in productivity and in the reliability of the programs produced. In this paper we describe a formal method for hierarchical program specification, implementation, and proof. We apply this method to a significant list processing problem and also discuss a number of extensions to current programming languages that ease hierarchical program design and proof.

References

[1]

Boyer, R.S., and Moore, JS. Private communication, June 1977.

[2]

Boyer, R.S., and Moore, JS. A lemma driven automatic theorem prover for recursive function theory. Proc. Int. Joint Conf. Artificial Intelligence, Cambridge, Mass., Aug. 1977.

[3]

BurstaU, R.M. Proving properties of programs by structural induction. Comptr. J. 12, 1 (Jan. 1969), 41-48.

[4]

Dalai, O.J., Mylirliaug, B., and Nygaard, K. Common base language, S-22. Norwegian Comptng. Ctr., Oslo, Norway, Oct. 1970.

[5]

Dahl, O.J., Dijkstra, E.W., and Hoare, C.A.R. Structured Programming. Academic Press, New York, 1972.

Digital Library

[6]

Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dept. of Comptr. Sci., U. of California, Berkeley, 1973.

[7]

Good, D.I. Provable programming. Proc. Int. Conf. Reliable Software, SIGPLAN Notices (ACM) 10, 6 (June 1975), 411-419.

Digital Library

[8]

Guttag, J. Abstract data types and the development of data structures. Comm. ACM 20, 6 (June 1977), 396-404.

Digital Library

[9]

Hoare, C.A.R. Proof of correctness of data representations. A cta Informatica 1, 4 (1972), 271-281.

[10]

Hoare, C.A.R., and Wirth, N. An axiomatic definition of the programming language PASCAL. Acta lnformatica 2, 4 (1973), 335-355.

[11]

Ichbiah, J.D., et al. The system implementation language LIS. Tech. Rep. 4549, E/EN, Compagnie Internationale pour l'Informatique, Louveciennes, France, Dec. 1974.

[12]

Igarashi, S., London, R.L., and Luckham, D.C. Automatic program verification I: A logical basis and its implementation. Acta Informatica 1, 4 (1975), 145-182.

[13]

An appraisal of program specifications. Computation Structures. Group Memo 141-1, Lab. for Comptr. Sci., M.I.T., Cambridge, Mass., April 1977.

[14]

Liskov, B., and ZiUes, S. Programming with abstract data types. Proc. ACM SIGPLAN Conf. Very High Level Languages, SIGPLAN Notices (ACM) 9, 4 (April 1974), 50-59.

Digital Library

[15]

Liskov, B., and Zilles, S. Specification techniques for data abstraction. IEEE Trans. Software Eng. SE-1, 1 (March 1975), 7-19.

Digital Library

[16]

McCarthy, J. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, Braffort and Hirschberg, Eds., North-Holland, Amsterdam, 1963, pp. 33-70.

[17]

McCarthy, J., et al. LISP 1.5 Programmer's Manual M.I.T. Press, Cambridge, Mass., 1962.

Digital Library

[18]

Manna, Z., Ness, S., and Vuillemin, J. Inductive methods for proving properties of programs. Comm. A CM 16, 8 (Aug. 1973), 491-502.

Digital Library

[19]

Moore, JS. The Interlisp virtual machine specification. Rep. CSL 76-5, Xerox Palo Alto Res. Ctr., Palo Alto, Calif., Sept. 1976.

[20]

-Morris, J. Protection in programming languages. Comm. A CM 16, 1 (Jan. 1973), 15-21.

Digital Library

[21]

Morris, J.M. Types are not sets. Proc. ACM Symposium on Principles of Programming Languages, Boston, Mass., Oct. 1973, pp. 120-124.

Digital Library

[22]

Neumann, P.G., et al. A provably secure operating'system: The system, its applications, and proofs. Final Rep., SRI Proj. 4332, SRI Int., Menlo Park, Calif., Feb. 1977.

[23]

Palme, J. Protected program modules in Simula 67. Res. Inst. of Nat. Defense, Stockholm, Sweden, July 1973.

[24]

Parnas, D.L. A technique for software module specification with examples. Comm. ACM 15, 5 (May 1972), 330-336.

Digital Library

[25]

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

Digital Library

[26]

Robinson, L., and Levitt, K.N. Proof techniques for hierarchically structured programs. Comm. ACM 20, 4 (April 1977), 271-283.

Digital Library

[27]

Robinson, L., et al. On attaining reliable software for a secure operating system. Proc. Int. Conf. Reliable Software, SIGPLAN Notices (ACM) 10, 6 (June 1975), 267-284.

Digital Library

[28]

Roubine, O., and Robinson, L. SPECIAL Reference Manual. Tech. Rep. CSL-45, SRI Project 4828, SRI Int., Menlo Park, Calif., 3rd ed., Jan. 1977.

[29]

Weghreit, B. The treatment of data types in EL 1. Comm. A CM 17, 5 (May 1974), 251-264.

Digital Library

[30]

Wegbreit, B., and Spitzen, J. M. Proving properties of complex data structures. J. ACM 23, 2 (April 1976), 389-396.

Digital Library

[31]

Wirth, N. Modula: A language for modular multiprogramming. Software--Practice and Experience 7 (1977), 3-35.

[32]

Wulf, W.A. ALPHARD: Toward a language to support structured programs. Comptr. Sci. Dept., Carnegie-Mellon U., Pittsburgh, Pa., April 1974.

[33]

Yourdon, E., and Constantine, L.L. Structured Design. Yourdon Press, New York, 1975.

Cited By

Wasserman A(2007)Information system design methodologyJournal of the American Society for Information Science10.1002/asi.463031010231:1(1-24)Online publication date: 22-Mar-2007
https://doi.org/10.1002/asi.4630310102
Morris J(2006)Programming by successive refinement of data abstractionsSoftware: Practice and Experience10.1002/spe.438010040210:4(249-263)Online publication date: 27-Oct-2006
https://doi.org/10.1002/spe.4380100402
Goguen JMeseguer J(2005)Universal realization, persistent interconnection and implementation of abstract modulesAutomata, Languages and Programming10.1007/BFb0012775(265-281)Online publication date: 22-Oct-2005
https://doi.org/10.1007/BFb0012775
Show More Cited By

Index Terms

Recommendations

Model-checking hierarchical structures

Hierarchical graph definitions allow a modular description of structures using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions allow us to specify structures of exponential size using ...
A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
What Is Object-Oriented Programming?

The meaning of the term 'object oriented' is examined in the context of the general-purpose programming language C++. This choice is made partly to introduce C++ and partly because C++ is one of the few languages that supports data abstraction, object-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 21, Issue 12

Dec. 1978

89 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/359657

Editor:
Robert L. Ashenhurst
The Univ. of Chicago, Chicago, IL

Issue’s Table of Contents

Copyright © 1978 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 1978

Published in CACM Volume 21, Issue 12

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
533
Total Downloads

Downloads (Last 12 months)115
Downloads (Last 6 weeks)9

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wasserman A(2007)Information system design methodologyJournal of the American Society for Information Science10.1002/asi.463031010231:1(1-24)Online publication date: 22-Mar-2007
https://doi.org/10.1002/asi.4630310102
Morris J(2006)Programming by successive refinement of data abstractionsSoftware: Practice and Experience10.1002/spe.438010040210:4(249-263)Online publication date: 27-Oct-2006
https://doi.org/10.1002/spe.4380100402
Goguen JMeseguer J(2005)Universal realization, persistent interconnection and implementation of abstract modulesAutomata, Languages and Programming10.1007/BFb0012775(265-281)Online publication date: 22-Oct-2005
https://doi.org/10.1007/BFb0012775
Pugh W(2005)Probabilistic analysis of set operations with constant-time set equality testAdvances in Computing and Information — ICCI '9010.1007/3-540-53504-7_62(62-71)Online publication date: 7-Jun-2005
https://doi.org/10.1007/3-540-53504-7_62
Hughes J(2005)Lazy memo-functionsFunctional Programming Languages and Computer Architecture10.1007/3-540-15975-4_34(129-146)Online publication date: 8-Jun-2005
https://doi.org/10.1007/3-540-15975-4_34
Acar UBlelloch GHarper R(2003)Selective memoizationACM SIGPLAN Notices10.1145/640128.60413338:1(14-25)Online publication date: 15-Jan-2003
https://dl.acm.org/doi/10.1145/640128.604133
Acar UBlelloch GHarper RAiken AMorrisett G(2003)Selective memoizationProceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/604131.604133(14-25)Online publication date: 15-Jan-2003
https://dl.acm.org/doi/10.1145/604131.604133
Kaplan HTarjan R(1999)Purely functional, real-time deques with catenationJournal of the ACM10.1145/324133.32413946:5(577-603)Online publication date: 1-Sep-1999
https://dl.acm.org/doi/10.1145/324133.324139
Kaplan HTarjan RLeighton FBorodin A(1995)Persistent lists with catenation via recursive slow-downProceedings of the twenty-seventh annual ACM symposium on Theory of computing10.1145/225058.225090(93-102)Online publication date: 29-May-1995
https://dl.acm.org/doi/10.1145/225058.225090
Owre SRushby JShankar Nvon Henke F(1995)Formal Verification for Fault-Tolerant ArchitecturesIEEE Transactions on Software Engineering10.1109/32.34582721:2(107-125)Online publication date: 1-Feb-1995
https://dl.acm.org/doi/10.1109/32.345827
Show More Cited By

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