Advertisement

Specware: Formal support for composing software

  • Yellamraju V. Srinivas
  • Richard Jüllig
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)

Abstract

Specware supports the systematic construction of formal specifications and their stepwise refinement into programs. The fundamental operations in Specware are that of composing specifications (via colimits), the corresponding refinement by composing refinements (via sheaves), and the generation of programs by composing code modules (via colimits). The concept of diagram refinement is introduced as a practical realization of composing refinements via sheaves. Sequential and parallel composition of refinements satisfy a distributive law which is a generalization of similar compatibility laws in the literature. Specware is based on a rich categorical framework with a small set of orthogonal concepts. We believe that this formal basis will enable the scaling to system-level software construction.

Keywords

Total Order Parallel Composition Definitional Extension Topological Sorting Signature Morphism 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Artin, M., Grothendieck, A., And Verdier, J. L. Théorie des Topos et Cohomologie Etale des Schémas, Lecture Notes in Mathematics, Vol. 269. Springer-Verlag, 1972. SGA4, Séminaire de Géométrie Algébrique du Bois-Marie, 1963–1964.Google Scholar
  2. 2.
    Bauer, F. L., Et Al. The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L, Lecture Notes in Computer Science, Vol. 183. Springer-Verlag, Berlin, 1985.Google Scholar
  3. 3.
    Bauer, F. L., Ehler, H., Horsch, A., Möller, B., Partsch, H., Paukner, O., and Pepper, P. The Munich Project CIP, Volume II: The Program Transformation System CIP-S, Lecture Notes in Computer Science, Vol. 292. Springer-Verlag, Berlin, 1987.Google Scholar
  4. 4.
    Bird, R. S. Introduction to the theory of lists. Tech. Rep. PRG-56, Oxford University Computing Laboratory, Programming Research Group, October 1986. Appeared in Logic of Programming and Calculi of Discrete Design, M. Broy, Ed., Springer-Verlag, NATO ASI Series F: Computer and Systems Sciences, Vol. 36, 1987.Google Scholar
  5. 5.
    Bird, R. A calculus of functions for program derivation. Tech. Rep. PRG-64, Oxford University, Programming Research Group, December 1987.Google Scholar
  6. 6.
    Blaine, L., And Goldberg, A. DTRE — a semi-automatic transformation system. In Constructing Programs from Specifications, B. Möller, Ed. North-Holland, Amsterdam, 1991, pp. 165–204.Google Scholar
  7. 7.
    Burstall, R. M., And Goguen, J. A. Putting theories together to make specifications. In Proceedings of the Fifth International Joint Conference on Artificial Intelligence (Cambridge, MA, August 22–25, 1977), IJCAI, pp. 1045–1058.Google Scholar
  8. 8.
    Gilham, L.-M., Goldberg, A., And Wang, T. C. Toward reliable reactive systems. In Proceedings of the 5th International Workshop on Software Specification and Design (Pittsburgh, PA, May 1989).Google Scholar
  9. 9.
    Goguen, J. A., And Burstall, R. M. CAT, A system for the correct elaboration of correct programs from structured specifications. Tech. Rep. CSL-118, SRI International, Oct. 1980.Google Scholar
  10. 10.
    Goguen, J. A., And Winkler, T. Introducing OBJ3. Tech. Rep. SRI-CSL-88-09, SRI International, Menlo Park, California, 1988.Google Scholar
  11. 11.
    Green, C. Synthesis of graphical displays for tabular data. Tech. Rep. SBIR.FR.86.1, Kestrel Institute, October 1987. Final Report for Phase I; Note: accompanying videotape.Google Scholar
  12. 12.
    Hoare, C. A. R. Proof of correctness of data representation. Acta Informatica 1 (1972), 271–281.Google Scholar
  13. 13.
    Jones, C. B. Systematic Software Development Using VDM. Prentice-Hall, Englewood Cliffs, NJ, 1986.Google Scholar
  14. 14.
    Jüllig, R. Applying formal software synthesis. IEEE Software 10, 3 (May 1993), 11–22. (also Technical Report KES.U.93.1, Kestrel Institute, May 1993).Google Scholar
  15. 15.
    Knuth, D. E. The Art of Computer Programming, Volume 1: Fundamental Algorithms. Addison-Wesley, Reading, Massachusetts, 1968.Google Scholar
  16. 16.
    Lambek, J., And Scott, P. J. Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge, 1986.Google Scholar
  17. 17.
    Lehman, M. M., Stenning, V., And Turski, W. M. Another look at software design methodology. ACM SIGSOFT Software Engineering Notes 9, 2 (April 1984), 38–53.Google Scholar
  18. 18.
    Mac Lane, S. Categories for the Working Mathematician. Springer-Verlag, New York, 1971.Google Scholar
  19. 19.
    Mac Lane, S., And Moerdijk, I. Sheaves in Geometry and Logic. Springer-Verlag, New York, 1992.Google Scholar
  20. 20.
    Meseguer, J. General logics. In Logic Colloquium'87, H.-D. Ebbinghaus et al., Eds. North-Holland, 1989, pp. 275–329.Google Scholar
  21. 21.
    Sannella, D., And Tarlecki, A. Specifications in an arbitrary institution. Inf. and Comput. 76 (1988), 165–210.Google Scholar
  22. 22.
    Sannella, D., And Tarlecki, A. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica 25, 3 (1988), 233–281.Google Scholar
  23. 23.
    Smith, D. R. KIDS — a semi-automatic program development system. IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering 16, 9 (September 1990), 1024–1043.Google Scholar
  24. 24.
    Smith, D. R. Constructing specification morphisms. Journal of Symbolic Computation, Special Issue on Automatic Programming 15, 5–6 (May–June 1993), 571–606.Google Scholar
  25. 25.
    Smith, D. R., And Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2–3 (October 1990), 305–321.Google Scholar
  26. 26.
    Srinivas, Y. V. A sheaf-theoretic approach to pattern matching and related problems. Theoretical Comput. Sci. 112 (1993), 53–97.Google Scholar
  27. 27.
    Turski, W. M., And Maibaum, T. E. The Specification of Computer Programs. Addison-Wesley, Wokingham, England, 1987.Google Scholar
  28. 28.
    Wirsing, M. Structured algebraic specifications: A kernel language. Theoretical Comput. Sci. 42 (1986), 123–249. A slight revision of his Habilitationsschrift, Technische Universität München, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Yellamraju V. Srinivas
    • 1
  • Richard Jüllig
    • 1
  1. 1.Kestrel InstitutePalo AltoUSA

Personalised recommendations