Writing Larch interface language specifications

ABSTRACT

Current research in specifications is emphasizing the practical use of formal specifications in program design. One way to encourage their use in practice is to provide specification languages that are accessible to both designers and programmers. With this goal in mind, the Larch family of formal specification languages has evolved to support a two-tiered approach to writing specifications. This approach separates the specification of state transformations and programming language dependencies from the specification of underlying abstractions. Thus, each member of the Larch family has a subset derived from a programming language and another subset independent of any programming languages. We call the former interface languages, and the latter the Larch Shared Language. This paper focuses on Larch interface language specifications. Through examples, we illustrate some salient features of Larch/CLU, a Larch interface language for the programming language CLU. We give an example of writing an interface specification following the two-tiered approach and discuss in detail issues involved in writing interface specifications and their interaction with their Shared Language components.

REFERENCES

• 1: ABRIAL, J. R. The specification language Z: Syntax and semantics. Programming Research Group, Oxford University, 1980.
• 2: GOGUEN, J. A., THATCHER, J. W., WAGNER, E. G., AND WRIGHT, J.B. Abstract data types as initial algebras and correctness of data representations. In Proceedings of the Conference on Computer Graphics, Pattern Recognition and Data Structures (May 1975), ACM, New York, 89-93.
• 3: ATREYA, S. K. Formal specification of a specification library. M.S. thesis, MIT, Dept. of Electrical Engineering and Computer Science, Cambridge, Mass., May 1982.
• 4: V. A. Berzins , Valdis A B?erzi?nes, ABSTRACT MODEL SPECIFICATIONS FOR DATA ABSTRACTIONS, Massachusetts Institute of Technology, Cambridge, MA, 1979
• 5: BIRKHOFr, G., AND LIPSON, J.D. Heterogeneous algebras. J. Comb. Theor. 8 (1970), 115-133.
• 6: The Vienna Development Method: The Meta-Language, January 1978
• 7: BURSTALL, R. M., AND GOGUEN, J. A. Putting theories together to make specifications. In Proceedings of the 5th International Joint Conference on Artificial Intelligence (Aug. 1977), 1045-1058. Invited paper.
• 8: BURSTALL, R. M., AND GOGUEN, J.A. An informal introduction to specifications using CLEAR. In The Correctness Problem in Computer Science, 1981.
• 9: CAINE, S. H., AND GORDON, E.K. PDL--A tool for software design. In Proceedings of the 1975 National Computer Conference (Anaheim, Calif., May 19-22). AFIPS Press, Reston, Va., 1975, 271-276.
• 10: EHRICH, H.-D. Extensions and implementations of abstract data type specifications. In Mathematical Foundations of Computer Science 1978, Proceedings. Lecture Notes in Computer Science, 64. Springer, New York, 1978, 155-164.
• 11: Hartmut Ehrig , Hans-Jörg Kreowski , James W. Thatcher , Eric G. Wagner , Jesse B. Wright, Parameterized Data Types in Algebraic Specification Languages (Short Version), Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.157-168, July 14-18, 1980
• 12: Hartmut Ehrig , B. Mahr, Fundamentals of Algebraic Specification I, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 13: R. Forgaard, A PROGRAM FOR GENERATING AND ANALYZING TERM REWRITING SYSTEMS, Massachusetts Institute of Technology, Cambridge, MA, 1984
• 14: GOGUEN, J. A. Abstract errors for abstract data types. In Proceedings of the IFIP Working Conference on Formal Basis of Programming Concepts (Aug. 1977). IFIP, 21.1-21.32.
• 15: GOGUEN, J. A., AND PARSAYE-GHOMI, K. Algebraic denotational semantics using parameterized abstract modules. CSL-119, Stanford Research Institute, Menlo Park, Calif., Feb. 1981.
• 16: GOOD, D. I., COHEN, R. M., HOCH, C. G., HUNTER, L. W., AND HARE, D. F. Report on the language Gypsy, version 2.0. ICSCA-CMP-10, Certifiable Minicomputer Project, Univ. of Texas, Austin, Sept. 1978.
• 17: John Vogel Guttag, The specification and application to programming of abstract data types., 1975
• 18: 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]
• 19: John Guttag , J. J. Horning, Formal specification as a design tool, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.251-261, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567471]
• 20: GUTTAG, J. V., HORNING, J. J., AND WING, J.M. Some notes on putting formal specifications to productive use. Sci. Comput. Program. 2, I (Oct. 1982), 53-68.
• 21: GUTTAG, J. V., AND HORNING, J. J. An introduction to the Larch Shared Language. In Proceedings of the IFIP 9th World Computer Congress (Paris, Sept. 1983), IFIP, 1983.
• 22: GUTTAG, J. V., HORNING, J. J., AND WING, J.M. The Larch family of specification languages. IEEE Softw. 2, 5 (Sept. 1985), 24-36.
• 23: GUTWAG, J. V., HORNINO, J. J., AND WING, J.M. Larch in five easy pieces. 5, DEC Systems Research Center, July 1985.
• 24: J V Guttag , J J Horning, Report on the Larch shared language, Science of Computer Programming, v.6 n.2, p.103-134, March 1986
• 25: J V Guttag , J J Horning, A Larch shared language handbook, Science of Computer Programming, v.6 n.2, p.135-157, March 1986
• 26: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 27: HOARE, C. A.R. Proof of correctness of data representations. Acta Inf. 1, 1 (1972), 271-281.
• 28: J J Horning, Combining algebraic and predicative specifications in Larch, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) on Formal Methods and Software, Vol.2: Colloquium on Software Engineering (CSE), p.12-26, June 1985, Berlin, Germany
• 29: HORNING, J.J. Cedar Mesa interface language. Private communication, 1983.
• 30: M. A. Jackson, Principles of Program Design, Academic Press, Inc., Orlando, FL, 1975
• 31: Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 32: Samuel Kamin, Final Data Types and Their Specification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.1, p.97-121, Jan. 1983 [doi>10.1145/357195.357202]
• 33: D. Kapur, TOWARDS A THEORY FOR ABSTRACT DATA TYPES, Massachusetts Institute of Technology, Cambridge, MA, 1980
• 34: KATZAN, H., JR. Systems Design and Documentation: An Introduction to the HIPO Method. Van Nostrand Reinhold, New York, 1976.
• 35: KOWNACKI, R. W. Semantic checking of formal specifications. M.S. thesis, MIT, Dept. of Electrical Engineering and Computer Science, Cambridge, Mass., Aug. 1984.
• 36: Pierre Lescanne, Computer experiments with the REVE term rewriting system generator, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.99-108, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567078]
• 37: LISKOV, B. H., AND ZILLES, S.N. Specification techniques for data abstractions. IEEE Trans. Softw. Eng. SE-I, 1 (1975), 7-19.
• 38: Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
• 39: LISKOV, B. H., AND BERZlNS, V. An appraisal of program specifications. Research Directions in Software Technology, Cambridge, Mass., 1979.
• 40: Barbara Liskov, CLU Reference Manual, Springer-Verlag New York, Inc., Secaucus, NJ, 1983
• 41: MUSSER, D.R. Abstract data type specification in the Affirm system. IEEE Trans. Softw. Eng. 6, 1 (Jan. 1980), 24-32.
• 42: NAKAJIMA, R., HONDA, M., AND NAKAHARA, H. Hierarchical program specification and verification--A many-sorted logical approach. Acta Inf. 14 (1980), 135-155.
• 43: R. Nakajima , T. Yuasa, Iota Programming System, Springer-Verlag New York, Inc., Secaucus, NJ, 1983
• 44: 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]
• 45: ROBINSON, L., AND ROUmNE, O. SPECIAL--A specification and assertion language. CSL-46, Stanford Research Institute, Menlo Park, Calif., Jan. 1977.
• 46: SCHEID, J., AND ANDERSON, S. The Ina Jo specification language reference manual. TM-(L)-6021/001/00, System Development Corp., Santa Monica, Calif., Mar. 1985.
• 47: STANDISH, T. A. Data structures: An axiomatic approach. Rep. 2639, Bolt, Beranek, and Newman, Cambridge, Mass., Aug. 1973.
• 48: SUFRIN, B., MORGAN, C., SORENSEN, I., AND HAYES, I. Notes for a Z handbook: Part 1--The mathematical language. Programming Research Group, Oxford Univ., Computing Laboratory, Aug. 1984.
• 49: James W. Thatcher , Eric G. Wagner , Jesse B. Wright, Data type specification: Parameterization and the power of specification techniques, Proceedings of the tenth annual ACM symposium on Theory of computing, p.119-132, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804340]
• 50: WAND, M. Final algebra semantics and data type extensions. J. Comput. Syst. Sc~ 19, 1 (Aug. 1979), 27-44.
• 51: J. M. Wing, A TWO-TIERED APPROACH TO SPECIFYING PROGRAMS, Massachusetts Institute of Technology, Cambridge, MA, 1983
• 52: WING, J.M. Helping specifiers evaluate their specifications. In Proceedings of the 2nd So{tware Engineering Conference (June 1984). AFCET, 179-191.
• 53: Edward Yourdon , Larry L. Constantine, Structured Design: Fundamentals of a Discipline of Computer Program and Systems Design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1979
• 54: ZACHARY, J. A syntax-directed tool for constructing specifications. M.S. thesis, MIT, Dept. of Electrical Engineering and Computer Science, Cambridge, Mass., Mar. 1983.
• 55: ZAVE, P. An operational approach to requirements specification for embedded systems. IEEE Trans. So{tw. Eng. 8, 3 (May 1982), 250-269.
• 56: ZILLES, S.N. Abstract specifications for data types. IBM Research Laboratory, San Jose, Calif., 1975.

INDEX TERMS

Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured); Languages
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Larch
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages; Procedures, functions, and subroutines; Abstract data types

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Specification techniques

General Terms:
Design, Languages, Verification