×

zbMATH — the first resource for mathematics

Logical systems for structured specifications. (English) Zbl 1061.68104
Summary: We study proof systems for reasoning about logical consequences and refinement of structured specifications, based on similar systems proposed earlier in the literature [D. Sannella and A. Tarlecki, Inf. Comput. 76, No. 2/3, 165–210 (1988; Zbl 0654.68017); M. Wirsing, in: F. L. Bauer et al. (eds.), Logic and algebra of specification, NATO ASI Series. Series F: Computer and Systems Sciences 94, 411–442 (1993; Zbl 0818.68109)]. Following Goguen and Burstall, the notion of an underlying logical system over which we build specifications is formalized as an institution and extended to a more general notion, called \((D,T)\)-institution. We show that under simple assumptions (essentially: amalgamation and interpolation) the proposed proof systems are sound and complete. The completeness proofs are inspired by proofs due to M. V. Cengarle [Formal specifications with higher-order parametrization. Ph.D. Thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, Berichte aus der Informatik. Aachen: Verlag Shaker (1994; Zbl 0921.68058)] for specifications in first-order logic and the logical systems for reasoning about them. We then propose a methodology for reusing proof systems built over institutions rich enough to satisfy the properties required for the completeness results for specifications built over poorer institutions where these properties need not hold.

MSC:
68Q65 Abstract data types; algebraic specification
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Software:
CoFI
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Astesiano, E.; Cerioli, M., Multiparadigm specification languagesa first attempt at foundations, (), 168-185 · Zbl 0812.68088
[2] Avron, A., Simple consequence relations, Inform. and comput., 91, 1, 105-139, (1991) · Zbl 0733.03007
[3] Bergstra, J.A.; Heering, J.; Klint, P., Module algebra, J. ACM, 37, 2, 335-372, (1990) · Zbl 0696.68040
[4] T. Borzyszkowski, Completeness of the logical system for structured specifications, in: F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, Selected Papers, 12th Internat. Workshop WADT’97, Tarquinia, Italy, Springer Lecture Notes in Computer Science, vol. 1376, Springer, Berlin, June 1997, pp. 107-121. · Zbl 0901.03028
[5] Borzyszkowski, T., Moving specification structures between logical systems, (), 16-28 · Zbl 0956.68031
[6] Burmeister, P., Partial algebras—survey of a unifying approach towards a two-valued model theory for partial algebras, Algebra univ., 15, 306-358, (1982) · Zbl 0511.03014
[7] Burmeister, P., A model theoretic approach to partial algebras, (1986), Akademie Verlag Berlin
[8] M.V. Cengarle, Formal specifications with high-order parameterization, Ph.D. Thesis, Institut für Informatik, Ludwig-Maximilians-Universität Müenchen, 1994. · Zbl 0921.68058
[9] Cerioli, M.; Meseguer, J., May i borrow your logic? (transporting logical structures along maps), Theoret. comput. sci., 173, 2, 311-347, (1997) · Zbl 0901.68186
[10] Chang, C.C.; Jerome Keisler, H., Model theory, studies in logic and the foundations of mathematics, (1973), North-Holland Amsterdam
[11] Diaconescu, R.; Goguen, J.; Stefaneas, P., Logical support for modularization, (), 83-130
[12] J. Farrés Casals, Verification in ASL and related specification languages, Ph.D. Thesis, Report CST-92-92, Dept. of Computer Science, University of Edinburgh, 1992.
[13] J.A. Goguen, R.M. Burstall, The semantics of Clear, a specification language, Proc. 1979 Copenhagen Winter School on Abstract Software Specification, Springer Lecture Notes in Computer Science, vol. 86, Springer, Berlin, 1980, pp. 292-332. · Zbl 0456.68024
[14] Goguen, J.A.; Burstall, R.M., Institutionsabstract model theory for specifications and programming, J. assoc. comput. Mach., 39, 95-146, (1992) · Zbl 0799.68134
[15] Goguen, J.A.; Meseguer, J., Completeness of many-sorted equational logic, Houston J. math., 11, 3, 307-334, (1985) · Zbl 0602.08004
[16] R. Hennicker, M. Bidoit, Observational logic, Tech. Report LSV-98-6, Lab. Specification et Verification, ENS de Cachan, France, 1998. · Zbl 1088.68112
[17] Harper, R.; Sannella, D.; Tarlecki, A., Structured theory presentations and logic representations, Ann. pure appl. logic, 67, 113-160, (1994) · Zbl 0809.03019
[18] E. Astesiano, B. Krieg-Brückner, H.J. Kreowski (Eds.), IFIP WG 1.3 Book on Algebraic Foundations of System Specification, Springer, Berlin, 1999.
[19] Kreisel, G.; Krivine, J.L., Elements of mathematical logic (model theory), (1967), North-Holland Amsterdam · Zbl 0155.33801
[20] Meseguer, J., General logic, (), 279-329
[21] T. Mossakowski, Representations, hierarchies, and graphs of institutions, Ph.D. Thesis, Fachbereich Mathematik und Informatik der Universität Bremen, 1996.
[22] P.D. Mosses, CoFI: the common framework initiative for algebraic specification and development, Theory and Practice of Software Development, Lecture Notes in Computer Science, vol. 1214, Springer, Berlin, 1997, pp. 115-137.
[23] P.H. Rodenburg, R.J. van Glabbeek, An interpolation theorem in equational logic, Report CS-R8838, Department of Computer Science, Center for Mathematics and Computer Science, Amsterdam, 1988.
[24] Salibra, A.; Scollo, G., Interpolation and compactness in categories of pre-institutions, Math. struct. comput. sci., 6, 3, 261-286, (1996) · Zbl 0860.03035
[25] D. Sannella, R. Burstall, Structured theories in LCF, Proc. 8th Colloq. on Trees in Algebra and Programming, L’Aquila, Lecture Notes in Computer Science, vol. 159, Springer, Berlin, 1983, pp. 377-391. · Zbl 0527.68070
[26] Sannella, D.; Sokołowski, S.; Tarlecki, A., Towards formal development of programs from algebraic specificationparameterization revisited, Acta inform., 29, 689-736, (1992) · Zbl 0790.68077
[27] Sannella, D.; Tarlecki, A., Specifications in an arbitrary institution, Inform. and comput., 76, 165-210, (1988) · Zbl 0654.68017
[28] Sannella, D.; Tarlecki, A., Essential concepts of algebraic specification and program development, Formal aspects comput., 9, 229-269, (1997) · Zbl 0887.68070
[29] A. Tarlecki, Bits and pieces of the theory of institutions, Proc. Workshop on Category Theory and Computer Programming, Guildford, Springer Lecture Notes in Computer Science, vol. 240, Springer, Berlin, 1986, pp. 334-363. · Zbl 0636.68029
[30] Tarlecki, A., Moving between logical systems, (), 478-502
[31] A. Tarlecki, Towards heterogeneous specifications, in: D. Gabbay, M. van Rijke (Eds.), Proc. of Internat. Workshop on Frontiers of Combining Systems FroCoS’98, Amsterdam, October 1998, Research Studies Press 2000, pp. 337-360. · Zbl 0988.03056
[32] Wirsing, M., Structured specifications: syntax, semantics and proof calculus, (), 411-442
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.