Conjunction as composition

ABSTRACT

Partial specifications written in many different specification languages can be composed if they are all given semantics in the same domain, or alternatively, all translated into a common style of predicate logic. The common semantic domain must be very general, the particular semantics assigned to each specification language must be conducive to composition, and there must be some means of communication that enables specifications to build on one another. The criteria for success are that a wide variety of specification languages should be accommodated, there should be no restrictions on where boundaries between languages can be placed, and intuitive expectations of the specifier should be met.

REFERENCES

• 1: Robert Allen , David Garlan, Towards Formalized Software Architectures, Carnegie Mellon University, Pittsburgh, PA, 1992
• 2: Alex Borgida , John Mylopoulos , Raymond Reiter, “…And nothing else changes”: the frame problem in procedure specifications, Proceedings of the 15th international conference on Software Engineering, p.303-314, May 17-21, 1993, Baltimore, Maryland, United States
• 3: ~BURSTALL, R.M. Formal description of program structure and semantics in first order logic. ~In B. Meltzer and D Michie, eds, Mochil~e Intelhgence 5 Edinburgh University Press, 1970, ~pp. 79-98.
• 4: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 5: Anthony Finkelstein , Michael Goedicke , Jeff Kramer , Celso Niskier, Viewpoint Oriented Software Development: Methods and Viewpoints in Requirements Engineering, Algebraic Methods II: Theory, Tools and Applications [papers from a workshop in Mierlo, The Netherlands, September 1989], p.29-54, September 01, 1989
• 6: ~FiNKELSTEIN, A., KRAMER, J., NUSEIBEH, }3, FINKELSTEIN, L, AND GOEDICKE, M Viewpoints ~A framework for integrating mulhple perspectives in system development Int. J. Sopw. ~Eng. Knowl. Eng 2, 1 (1992), 31 57
• 7: David Garlan , David Notkin, Formalizing Design Spaces: Implicit Invocation Mechanisms, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.31-44, October 21-25, 1991
• 8: ~HAILPERN, B. Multiparadlgm languages and environments (guest editor's introduction to a ~special issue) IEEE Softw. 3, i (Jan. 1986), 6-9.
• 9: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 10: David Harel , Amir Pnueli , Hagi Lachover , Amnon Naamad , Michal Politi , Rivi Sherman , Aharon Shtull-Trauring , Mark Trakhtenbrot, STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.403-414, April 1990 [doi>10.1109/32.54292]
• 11: Roger Hayes , Richard D. Schlichting, Facilitating mixed language programming in distributed systems, IEEE Transactions on Software Engineering, v.13 n.12, p.1254-1264, December 1, 1987 [doi>10.1109/TSE.1987.232879]
• 12: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 13: ~INTERNATIONAL ORGANIZATION FOR STANDARDIZATION. Informatmn processing systems Open ~systems interconnectmn--LOTOS--A formal description technique based on the temporal ~ordering' of' observatmnal behaviour. ISO 8807.1989
• 14: M. A. Jackson, Principles of Program Design, Academic Press, Inc., Orlando, FL, 1975
• 15: ~JACKSON, M. Some complexities m computer-based systems and their mlphcatlons for ~system development. In Proeeedzngs of CompEuro '90. IEEE Computer Society, (ISBN ~0-8186-2041-2), 1990, pp. 344-351.
• 16: ~JACKSON, M., AND ZAVE, P. Domain descriptions In Proceedings of the 1EE~' lnternatmnal ~Symposium on Requirements Engineering. IEEE Computer Society Press (ISBN 0-8186- ~3120-1), 1993, pp. 56 64.
• 17: W. Lewis Johnson , Martin S. Feather , David R. Harris, Representation and Presentation of Requirements Knowledge, IEEE Transactions on Software Engineering, v.18 n.10, p.853-869, October 1992 [doi>10.1109/32.163603]
• 18: C B Jones, Systematic software development using VDM, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1986
• 19: ~KLEENE, S C Mathematmal Log'm. Wiley, 1967.
• 20: Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989 [doi>10.1145/63238.63240]
• 21: ~LAMP(roT, L. A temporal logic of actmns DEC Systems Research Center 57, Palo Alto, ~Califorma, Apr. 1990
• 22: ~LONDON, P. E., AND FEATHER, M S Implementing specificatmn freedoms SoL Comput. ~Prog 2, (1982), 91-131
• 23: Brendan P. Mahony , Ian J. Hayes, A Case-Study in Timed Refinement: A Mine Pump, IEEE Transactions on Software Engineering, v.18 n.9, p.817-826, September 1992 [doi>10.1109/32.159841]
• 24: Nico Plat , Jan van Katwijk , Kees Pronk, A Case for Structured Analysis/Formal Design, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.81-105, October 21-25, 1991
• 25: ~PNUELI, A. The temporal logic of programs. In Proceedings of the 18th Annual Symposium ~ on Foundations of Computer Smence. }EEE Computer Socmty (77CH1278-1), 1977, pp ~46- 57
• 26: ~REiSS, S P Working in the Garden environment for conceptual programming. IEEE ~Software ~, 6 (Nov 1987), 16-27.
• 27: J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 28: P T Ward, The transformation schema: An extension of the data flow diagram to represent control and timing, IEEE Transactions on Software Engineering, v.12 n.2, p.198-210, Feb. 1986
• 29: ~WINE, D S. Integrating syntaxes and their associated semantics. USC/Informatlon Sm- ~ences Institute Tech Rep RR-92-297 Umv Southern Calif., Marina de} Rey, Calif., 1992
• 30: Jack C. Wileden , Alexander L. Wolf , William R. Rosenblatt , Peri L. Tarr, Specification-level interoperability, Communications of the ACM, v.34 n.5, p.72-87, May 1991 [doi>10.1145/103167.103175]
• 31: Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990 [doi>10.1109/2.58215]
• 32: J. B. Wordsworth, Software Development with Z: A Practical Approach to Formal Methods in Software Engineering, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1992
• 33: Pamela Zave, A Compositional Approach to Multiparadigm Programming, IEEE Software, v.6 n.5, p.15-25, September 1989 [doi>10.1109/52.35586]
• 34: ~ZAVE, P., AND JACKSON, M. Composition of descriptions: A progress report. In Proceedings of ~the Formal Methods Workshop '91. Sprmger-Verlag, New York, 1991.
• 35: Pamela Zave , Michael Jackson, Techniques for Partial Specification and Specification of Switching Systems, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.511-525, October 21-25, 1991
• 36: ~ZAVE, P., AND JACKSON, M. Where do operations come from? Specification of event proper- ~ties, submitted for publication, 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)

General Terms:
Languages, Theory, Verification

Keywords:
compositional specification, multiparadigm specification, practical specification