Abstract
The main aim of this paper is to present a completeness proof of a formal system for reasoning about logical consequences of structured specifications. The system is based on the proof rules for structural specifications build in an arbitrary institution as presented in [ST 88]. The proof of its completeness is inspired by the proof due to M. V. Cengarle (see [Cen 94]) for specifications in first-order logic and the logical system for reasoning about them presented also in [Wir 91].
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. L. Bell, M. Machover. A course in mathematical logic. North-Holland, 1986.
J. A. Bergstra, J. Heering, P. Klint. Module algebra. Journal of the ACM, 37(2):335–372, April 1990.
M. V. Cengarle. Formal Specifications with High-Order Parameterization. Ph.D. thesis, Institut für Informatik, Ludwig-Maximilians-Universität Müenchen, 1994.
R. Diaconescu, J. Goguen, P. Stefaneas. Logical Support for Modularization. In: G. Huet, G. Plotkin, editors Logical Environments, Proceedings of a Workshop held in Edinburgh, Scotland, May 1991, Cambridge University Press, pages 83–130, 1993.
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.
J. A. Goguen, R. M. Burstall. Institutions: abstract model theory for specifications and programming. Report ECS-LFCS-90-106, University of Edinburgh, 1990.
J. A. Goguen, J.Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, volume. 11(3), pages 307–334, 1985.
P. D. Mosses. CoFI: The Common Framework Initiative for Algebraic Specification and Development. Theory and Practice of Software Development, volume 1214 of LNCS, pages 115–137, Springer-Verlag, 1997.
D. Sannella, R. Burstall. Structured Theories in LCF. Proc. 8th Colloq. on Trees in Algebra and Programming, L'Aquila, LNCS 159, pp. 377–391, Springer 1983.
D. Sannella, S. Sokolowski, A. Tarlecki. Towards formal development of programs from algebraic specification: parameterization revised. Acta Informatica, volume 29, pages 689–736, 1992.
D. Sannella, A. Tarlecki. Specifications in an Arbitrary Institution Information and Computation, volume 76, pages 165–210, 1988.
D. Sannella, A. Tarlecki. Essential concepts of algebraic specification and program development. To appear in: Formal Aspects of Computing.
A. Tarlecki. Bits and pieces of the theory of institutions. Proc. Workshop on Category Theory and Computer Programming, Guildford. Springer LNCS 240, pages 334–363, 1986.
A. Tarlecki. Moving between logical systems. Recent Trends in Data Type Specifications. Selected Papers. 11th Workshop on Specification of Abstract Data Types ADT'95, Olso, September 1995, eds. M. Haveraaen, O. J. Dahl, O. Owe, Springer LNCS 1130, pages 478–502, 1996.
M. Wirsing. Structured Specifications: Syntax, Semantics and Proof Calculus. In F. L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, volume 94 of NATO ASI Series F: Computer and Systems Sciences, pages 411–442. Springer Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Borzyszkowski, T. (1998). Completeness of a logical system for structured specifications. In: Presicce, F.P. (eds) Recent Trends in Algebraic Development Techniques. WADT 1997. Lecture Notes in Computer Science, vol 1376. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-64299-4_29
Download citation
DOI: https://doi.org/10.1007/3-540-64299-4_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64299-2
Online ISBN: 978-3-540-69719-0
eBook Packages: Springer Book Archive