×

Category localization semantics for specification refinements. (English) Zbl 1124.68063

Summary: We describe the theory of refinements of specifications based on localizations of categories. The approach allows us to enlarge the family of refinements (i.e. specification morphisms) of the category Spec – the category of first-order theories (specifications) of multi-sorted algebras. We prove that the class of specification morphisms in the category Spec can be enriched by the class of all interpretations of theories from Spec in all definitional extensions of theories of multi-sorted algebras. It provides a guide for finding a path leading from a given specification to a specification which is a provably correct code in a programming language (like C\(++\), Lisp, Java).

MSC:

68Q65 Abstract data types; algebraic specification
18C10 Theories (e.g., algebraic theories), structure, and semantics
18E35 Localization of categories, calculus of fractions

Software:

DTRE; Specware
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Blaine, L., Goldberg, A.: DTRE – a semi-automatic transformation system, in constructing programs from specifications. In: Moller, B. (ed.) Constructing Programs from Specifications. North Holland (1991)
[2] Burstall, R.M., Goguen, J.A.: The semantics of clear, a specification language. In: Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, LNCS, vol. 86, pp. 292–332. Springer, Berlin Heidelberg New York (1979) · Zbl 0456.68024
[3] Cohn, P.M.: Free Rings and their Relations. Academic (1985) · Zbl 0659.16001
[4] Ehrig, H.: Bigraphs meet double pushouts. EATCS Bulletin, vol. 78, pp. 72–85 (October 2002) · Zbl 1169.68450
[5] Faber, M., Vogel, P.: The Cohn localization of the free group rings. Math. Proc. Comb. Phil. Soc., III 433 (1992)
[6] Gabriel, P., Zisman, M.: Calculus of Fractions and Homotopy Theory. Springer, Berlin Heidelberg New York (1967) · Zbl 0186.56802
[7] Goguen, J.A.: Mathematical representation of hierarchically organized systems. In: Attinger, E., Karger, S. (eds.) Global Systems Dynamics, pp. 112–128 (1971)
[8] Goguen, J.A., Burstall, R.M.: A study in the foundations of programming methodology: specifications, institutions, charters and parchments. In: Pitt, D., et al. (eds.) Category Theory and Computer Programming, LNCS, vol. 240, pp. 313–333 (1985) · Zbl 0615.68002
[9] Jullig, R., Srinivas, Y.V.: Specware Manual. Kestrel Institute (1992)
[10] Kokar, M., Tomasik, J., Weyman, J.: Application of localizations of categories to fusion. No.90 LLAIC (2000) (Preprint)
[11] Kokar, M.M., Tomasik, J., Weyman, J.: Formalizing classes of information fusion systems. Information Fusion : an International Journal on Multi-Sensor, Multi-Source Information Fusion vol. 5, pp. 189–202 (2004)
[12] Mossakowski, T., Tarlecki, A., Pawłowski, W.: Combining and representing logical systems. In: Moggi, E. (ed.) Category Theory and Computer Programming, LNCS, vol. 1290, pp. 177–198. Springer, Berlin Heidelberg New York (1997) · Zbl 0881.03044
[13] Smith, D.: KIDS: a knowledge based software development system, in automating software design. In: Lowry, M., McCartney, R. (eds.) Automating Software Design. MIT Press (1991)
[14] Srinivas, Y.V., Jullig, R.: Specware: formal support for composing software. In: Proceedings of the Conference of Mathematics of Program Construction. Kloster Irsee, Germany (1995)
[15] Tarlecki, A., Goguen, J.A., Burstall, R.M.: Some fundamental algebraic tools for the semantics of computation. Part III: Indexed categories. Theor. Comp. Sci. 91, 239–264 (1991) · Zbl 0755.18004 · doi:10.1016/0304-3975(91)90085-G
[16] Uschold, M., et al.: Ontology reuse and application. In: Proceedings of the First International Conference on Formal Ontology in Information Systems. Trento (1998)
[17] Waldiger, R., et al.: Specware Language Manual 2.0.1. Suresoft,Inc. (1996)
[18] Wang, T.C., Goldberg, A.: A mechanical verifier for supporting the design of reliable reactive systems. International Symposium on Software Reliability Engineering. Austin, Texas (1996)
[19] Wiliamson, K., Healy, M.: Boeing Applied Research and Technology. Bellevue, Washington, 20 March (1998)
[20] Wiliamson, K., Ridle, P.: Knowledge repositories for multiple uses, Goddard conference on space applications of artificial intelligence. Goddard Conference on Space Applications of Artificial Intelligence. Deriving Engineering Software from Requirement, pp. 353–367 (1991)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.