An example of hierarchical design and proof

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: Ole Johan Dahl, Structured Programming, Academic Press, Inc., Orlando, FL, 1972
• 6: Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dept. of Comptr. Sci., U. of California, Berkeley, 1973.
• 7: Donald I. Good, Provable programming, Proceedings of the international conference on Reliable software, p.411-419, April 21-23, 1975, Los Angeles, California
• 8: John Guttag, Abstract data types and the development of data structures, Communications of the ACM, v.20 n.6, p.396-404, June 1977 [doi>10.1145/359605.359618]
• 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: Barbara Liskov , Stephen Zilles, Programming with abstract data types, Proceedings of the ACM SIGPLAN symposium on Very high level languages, p.50-59, March 28-29, 1974, Santa Monica, California, United States
• 15: Liskov, B., and Zilles, S. Specification techniques for data abstraction. IEEE Trans. Software Eng. SE-1, 1 (March 1975), 7-19.
• 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: John McCarthy, LISP 1.5 Programmer's Manual, The MIT Press, 1962
• 18: Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973 [doi>10.1145/355609.362336]
• 19: Moore, JS. The Interlisp virtual machine specification. Rep. CSL 76-5, Xerox Palo Alto Res. Ctr., Palo Alto, Calif., Sept. 1976.
• 20: James H. Morris, Jr., Protection in programming languages, Communications of the ACM, v.16 n.1, p.15-21, Jan. 1973 [doi>10.1145/361932.361937]
• 21: James B. Morris, Programming by semantic refinement, Proceeding of ACM SIGPLAN - SIGOPS interface meeting on Programming languages - operating systems, p.120-122, January 1973
• 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: D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
• 25: D. L. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, v.15 n.12, p.1053-1058, Dec. 1972 [doi>10.1145/361598.361623]
• 26: Lawrence Robinson , Karl N. Levitt, Proof techniques for hierarchically structured programs, Communications of the ACM, v.20 n.4, p.271-283, April 1977 [doi>10.1145/359461.359483]
• 27: Lawrence Robinson , Karl N. Levitt , Peter G. Neumann , Ashok R. Saxena, On attaining reliable software for a secure operating system, Proceedings of the international conference on Reliable software, p.267-284, April 21-23, 1975, Los Angeles, California
• 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: Ben Wegbreit, The treatment of data types in EL1, Communications of the ACM, v.17 n.5, p.251-264, May 1974 [doi>10.1145/360980.360992]
• 30: Ben Wegbreit , Jay M. Spitzen, Proving Properties of Complex Data Structures, Journal of the ACM (JACM), v.23 n.2, p.389-396, April 1976 [doi>10.1145/321941.321957]
• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages

General Terms:
Design, Languages, Performance, Theory, Verification

Keywords:
data abstraction, hierarchical structures, program verification, software modules, specification