Abstract
Development graphs are a tool for dealing with structured specifications in a formal program development in order to ease the management of change and reusing proofs. In this work, we extend development graphs with hiding (e.g. hidden operations). Hiding is a particularly difficult to realize operation, since it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolute complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system (and thus also does not prescribe the nature of the parts of a specification that may be hidden).
Chapter PDF
Similar content being viewed by others
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.
References
S. Autexier, D. Hutter, H. Mantel, and A. Schairer. Towards an evolutionary formal software-development using CASL. In C. Choppy, D. Bert, and P. Mosses, (Eds.), Recent Developments in Algebraic Development Techniques, 14th International Workshop, WADT’99, Bonas, France, LNCS 1827, page 73–88, Springer-Verlag, 2000.
S. Autexier, D. Hutter, H. Mantel, A. Schairer. System Description: Inka 5.0-A Logic Voyager. In H. Ganzinger, (Ed.), Proceedings of CADE-16, Trento, Italy, LNAI 1632, Springer-Verlag, 1999.
J. Adámek, J. Rosický. Locally Presentable and Accessible Categories, Cambridge University Press, 1994.
T. Borzyszkowski. Logical systems for structured specifications. Theoretical Computer Science. To appear.
CoFI Language Design Task Group. The Common Algebraic Specification Language ( Casl)-Summary, Version 1.0 and additional Note S-9 on Semantics, available from http://www.brics.dk/Projects/CoFI, 1998.
M. Cerioli, J. Meseguer. May I borrow your logic?, Theoretical Computer Science, 173:311–347, 1997.
R. Diaconescu, J. Goguen, P. Stefaneas. Logical support for modularization, In G. Huet, G. Plotkin, (Eds), Workshop on Logical Frameworks, 1991.
J. A. Goguen and R. M. Burstall: Institutions: Abstract model theory for specification and programming, Journal of the Association for Computing Machinery, 39:95–146, 1992. Predecessor in: LNCS 164, 221-256, 1984.
R. Hennicker, M. Wirsing, M. Bidoit. Proof systems for structured speci-cations with observability operators, Theoretical Computer Science, 173(2):393–443, 1997.
R. Harper, D. Sannella, A. Tarlecki. Structured presentations and logic representations, In Annals of Pure and Applied Logic, 67:113–160, 1994.
J. Meseguer. General logics, In Logic Colloquium 87, pages 275–329, North Holland, 1989.
T. Mossakowski, Kolyang, B. Krieg-Bruckner. Static semantic analysis and theorem proving for CASL, In 12th Workshop on Algebraic Development Techniques, Tarquinia, LNCS 1376, pages 333–348, Springer-Verlag, 1998.
D. Sannella, A. Tarlecki. Specifications in an arbitrary institution, Information and Computation, 76(2-3):165–210, 1988.
D. Sannella, A. Tarlecki. Towards Formal Development of Programs from Algebraic Specifications: Model-Theoretic Foundations, 19th ICALP, Springer, LNCS 623, pages 656–671, Springer-Verlag, 1992.
L. Schroder, T. Mossakowski, P. Hoffman, B. Klin, and A. Tarlecki. Semantics for architectural specifications in CASL, In H. Hußmann, (Ed.), Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), Genova, Italy, 2001.
D. Hutter et. al. Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, pages 523–530, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T., Autexier, S., Hutter, D. (2001). Extending Development Graphs with Hiding. In: Hussmann, H. (eds) Fundamental Approaches to Software Engineering. FASE 2001. Lecture Notes in Computer Science, vol 2029. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45314-8_20
Download citation
DOI: https://doi.org/10.1007/3-540-45314-8_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41863-4
Online ISBN: 978-3-540-45314-7
eBook Packages: Springer Book Archive