Abstract
Goguen emphasized long ago that colimits are how to compose systems [7]. This paper corroborates and elaborates Goguen’s vision by presenting a variety of situations in which colimits can be mechanically applied to support software development by refinement. We illustrate the use of colimits to support automated datatype refinement, algorithm design, aspect weaving, and security policy enforcement.
Keywords
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Becker, M., Gilham, L., Smith, D.R.: Planware II: Synthesis of schedulers for complex resource systems. Tech. rep., Kestrel Technology (2003)
Burstall, R.M., Goguen, J.A.: Putting theories together to make specifications. In: Proceedings of the Fifth International Joint Conference on Artificial Intelligence IJCAI, Cambridge, MA, August 22–25, pp. 1045–1058 (1977)
Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification languge. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, Springer, Heidelberg (1980)
Coglio, A.: Toward automatic generation of provably correct Java Card applets. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, Springer, Heidelberg (2003)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252. ACM, New York (1977)
Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI 2002 (2002)
Goguen, J.: Categorical foundations for general systems theory. In: Pichler, F., Trappl, R. (eds.) Advances in Cybernetics and Systems Research Transcripta Books, pp. 121–130 (1973)
Goguen, J.A.: Parameterized programming. IEEE Transactions on Software Engineering SE-10 5, 528–543 (1984)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for computer science. Journal of the ACM 39(1), 95–146 (1992)
Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI 2002 (2002)
Goguen, J., Burstall, R.: CAT: a system for the structured elaboration of correct programs from structured specifications. Tech. Rep. CSL-118, SRI International (1988)
Kestrel Institute. Specware System and documentation (2003), http://www.specware.org/
Kiczales, G., et al.: An Overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)
Papadimitriou, C.H., Steiglitz, K.: Combinatorial Optimization: Algorithms and Complexity. Prentice Hall, Englewood Cliffs (1982)
Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: Proceedings of Automated Software Engineering Conference, pp. 157–165. IEEE Computer Society Press, Los Alamitos (2001)
Pavlovic, D., Smith, D.R.: Evolving specifications. Tech. rep., Kestrel Institute (2004)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of the Twenty-Second ACM Symposium on Principles of Programming Languages, pp. 49–61. ACM, New York (1995)
Schneider, F.: Enforceable security policies. ACM Transactions on Information and System Security 3(1), 30–50 (2000)
Smith, D.R.: KIDS – a semi-automatic program development system. In: IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering, vol. 16(9), pp. 1024–1043 (1990)
Smith, D.R.: Constructing specification morphisms. Journal of Symbolic Computation, Special Issue on Automatic Programming 15 (5-6), 571–606 (1993)
Smith, D.R.: Toward a classification approach to design. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 62–84. Springer, Heidelberg (1996)
Smith, D.R.: Designware: Software development by refinement. In: Hoffman, M., Pavlovic, D., Rosolini, P. (eds.) Proceedings of the Eighth International Conference on Category Theory and Computer Science, pp. 355–370 (1999)
Smith, D.R.: Mechanizing the development of software. In: Broy, M., Steinbrueggen, R. (eds.) Calculational System Design, Proceedings of the NATO Advanced Study Institute, pp. 251–292. IOS Press, Amsterdam (1999)
Smith, D.R.: A generative approach to aspect-oriented programming. In: Karsai, G., Visser, E. (eds.) GPCE 2004. LNCS, vol. 3286, pp. 39–54. Springer, Heidelberg (2004)
Smith, D.R., Havelund, K.: Automatic enforcement of error-handling policies. Tech. rep., Kestrel Technology (September 2004)
Smith, D.R., Lowry, M.R.: Algorithm theories and design tactics. Science of Computer Programming 14(2-3), 305–321 (1990)
Smith, D.R., Parra, E.A., Westfold, S.J.: Synthesis of planning and scheduling software. In: Tate, A. (ed.) Advanced Planning Technology, pp. 226–234. AAAI Press, Menlo Park (1996)
Srinivas, Y.V., Jüllig, R.: Specware: Formal support for composing software. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 399–422. Springer, Heidelberg (1995)
The Open Group. Security design patterns. Tech. rep. (2004), http://www.opengroup.org/security/gsp.htm
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Smith, D.R. (2006). Composition by Colimit and Formal Software Development. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_17
Download citation
DOI: https://doi.org/10.1007/11780274_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35462-8
Online ISBN: 978-3-540-35464-2
eBook Packages: Computer ScienceComputer Science (R0)