Hostname: page-component-78c5997874-m6dg7 Total loading time: 0 Render date: 2024-11-10T00:35:52.024Z Has data issue: false hasContentIssue false
  • English
  • Français

Observational interpretation of Casl specifications

Published online by Cambridge University Press:  01 April 2008

MICHEL BIDOIT ,
DONALD SANNELLA  and
ANDRZEJ TARLECKI
MICHEL BIDOIT
Affiliation:
Laboratoire Spécification et Vérification, CNRS & ENS de Cachan, France Website: www.lsv.ens-cachan.fr/~bidoit/
DONALD SANNELLA
Affiliation:
Laboratory for Foundations of Computer Science, University of Edinburgh, United Kingdom Website: homepages.inf.ed.ac.uk/dts/
ANDRZEJ TARLECKI
Affiliation:
Institute of Informatics, Warsaw University, and Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland Website: www.mimuw.edu.pl/~tarlecki/
Get access Rights & Permissions [Opens in a new window]

Abstract

We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduces some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 18 , Issue 2 , April 2008 , pp. 325 - 371
Copyright
Copyright © Cambridge University Press 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P. D., Sannella, D. and Tarlecki, A. (2002) Casl: The Common Algebraic Specification Language. Theoretical Computer Science 286 153–196.CrossRefGoogle Scholar
Astesiano, E., Krieg-Brückner, B. and Kreowski, H.-J. (1999) (eds.) Algebraic Foundations of Systems Specification, Springer.CrossRefGoogle Scholar
Baumeister, H., Cerioli, M., Haxthausen, A., Mossakowski, T., Mosses, P. D., Sannella, D. and Tarlecki, A. (2004) Casl Semantics. In: Mosses, P. D. (ed.) Casl Reference Manual. Springer-Verlag Lecture Notes in Computer Science 2960 115–273.Google Scholar
Bernot, G. (1987) Good functors . . . are those preserving philosophy! Proc. 2nd Summer Conf. on Category Theory and Computer Science CTCS'87. Springer-Verlag Lecture Notes in Computer Science 283 182–195.CrossRefGoogle Scholar
Bidoit, M. and Hennicker, R. (1993) A general framework for modular implementations of modular systems. Proc. 4th Intl. Conf. on Theory and Practice of Software Development TAPSOFT'93. Springer-Verlag Lecture Notes in Computer Science 668 199–214.CrossRefGoogle Scholar
Bidoit, M. and Hennicker, R. (1998) Modular correctness proofs of behavioural implementations. Acta Informatica 35 (11)951–1005.CrossRefGoogle Scholar
Bidoit, M. and Hennicker, R. (2006) Proving behavioral refinements of COL-specifications. Algebra, Meaning and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday. Springer-Verlag Lecture Notes in Computer Science 4060 333–354.CrossRefGoogle Scholar
Bidoit, M., Hennicker, R. and Wirsing, M. (1995) Behavioural and abstractor specifications. Science of Computer Programming 25 149–186.CrossRefGoogle Scholar
Bidoit, M. and Mosses, P. D. (2004) Casl User Manual. Springer-Verlag Lecture Notes in Computer Science 2900.CrossRefGoogle Scholar
Bidoit, M., Sannella, D. and Tarlecki, A. (2002a) Architectural specifications in Casl. Formal Aspects of Computing 13 252–273.CrossRefGoogle Scholar
Bidoit, M., Sannella, D. and Tarlecki, A. (2002b) Global development via local observational construction steps. Proc. 27th Intl. Symp. on Mathematical Foundations of Computer Science, MFCS'02. Springer-Verlag Lecture Notes in Computer Science 2420 1–24.CrossRefGoogle Scholar
Bidoit, M., Sannella, D. and Tarlecki, A. (2004) Toward component-oriented formal software development: an algebraic approach. Proc. 9th Monterey Workshop, Radical Innovations of Software and Systems Engineering in the Future, Venice, October 2002. Springer-Verlag Lecture Notes in Computer Science 2941 75–90.CrossRefGoogle Scholar
Bidoit, M. and Tarlecki, A. (1996) Behavioural satisfaction and equivalence in concrete model categories. Proc. 20th Coll. on Trees in Algebra and Computing CAAP'96, Linköping. Springer-Verlag Lecture Notes in Computer Science 1059 241–256.CrossRefGoogle Scholar
Burmeister, P. (1986) A Model Theoretic Approach to Partial Algebras, Akademie Verlag.Google Scholar
Burstall, R. and Goguen, J. (1980) The semantics of Clear, a specification language. Proc. Advanced Course on Abstract Software Specifications, Copenhagen. Springer-Verlag Lecture Notes in Computer Science 86 292–332.CrossRefGoogle Scholar
The CoFI Language Design Group (2004) Casl Summary. Krieg-Brückner, B. and Mosses, P. D. (eds.) In: Mosses, P. D. (ed.) Casl Reference Manual. Springer-Verlag Lecture Notes in Computer Science 2960 3–74.Google Scholar
Ehrig, H. and Kreowski, H.-J. (1999) Refinement and implementation. In: Astesiano, E., Krieg-Brückner, B. and Kreowski, H.-J. (eds.) Algebraic Foundations of Systems Specification, Springer 201–242.CrossRefGoogle Scholar
Ehrig, H., Kreowski, H.-J., Mahr, B. and Padawitz, P. (1982) Algebraic implementation of abstract data types. Theoretical Computer Science 20 209–263.CrossRefGoogle Scholar
Ehrig, H. and Mahr, B. (1985) Fundamentals of Algebraic Specification I: Equations and Initial Semantics, Springer.CrossRefGoogle Scholar
Ganzinger, H. (1983) Parameterized specifications: parameter passing and implementation with respect to observability. ACM Transactions on Programming Languages and Systems 5 318–354.CrossRefGoogle Scholar
Giarratana, V., Gimona, F. and Montanari, U. (1976) Observability concepts in abstract data type specifications. Proc. 5th Intl. Symp. on Mathematical Foundations of Computer Science. Springer-Verlag Lecture Notes in Computer Science 45 576–587.CrossRefGoogle Scholar
Ginzburg, A. (1968) Algebraic Theory of Automata, Academic Press.Google Scholar
Goguen, J. and Burstall, R. (1992) Institutions: abstract model theory for specification and programming. Journal of the ACM 39 95–146.CrossRefGoogle Scholar
Goguen, J., Thatcher, J. and Wagner, E. (1978) An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Yeh, R. T. (ed.) Current Trends in Programming Methodology, Vol. 4: Data Structuring, Prentice-Hall, 80–149.Google Scholar
Guttag, J. and Horning, J. (1993) Larch: Languages and Tools for Formal Specification, Springer.CrossRefGoogle Scholar
Hoare, C. A. R. (1972) Proofs of correctness of data representations. Acta Informatica 1 271–281.CrossRefGoogle Scholar
Hoffman, P. (2001) Verifying architectural specifications. Recent Trends in Algebraic Development Techniques, Selected Papers, WADT'01. Springer-Verlag Lecture Notes in Computer Science 2267 152–175.CrossRefGoogle Scholar
Honsell, F., Longley, J., Sannella, D. and Tarlecki, A. (2000) Constructive data refinement in typed lambda calculus. Proc. 2nd Intl. Conf. on Foundations of Software Science and Computation Structures. Springer-Verlag Lecture Notes in Computer Science 1784 149–164.Google Scholar
Kahrs, S., Sannella, D. and Tarlecki, A. (1997) The definition of Extended ML: a gentle introduction. Theoretical Comp. Sci. 173 445–484.CrossRefGoogle Scholar
Klin, B., Hoffman, P., Tarlecki, A., Schröder, L. and Mossakowski, T. (2001) Checking amalgamability conditions for Casl architectural specifications. Proc. 26th Intl. Symp. on Mathematical Foundations of Computer Science MFCS'01. Springer-Verlag Lecture Notes in Computer Science 2136 451–463.CrossRefGoogle Scholar
Milner, R. (1971) An algebraic definition of simulation between programs. Proc. 2nd Intl. Joint Conf. on Artificial Intelligence, London 481–489.Google Scholar
Mossakowski, T., Hoffman, P., Autexier, S. and Hutter, D. (2004) Casl Logic. In: Mosses, P. D. (ed.) Casl Reference Manual. Springer-Verlag Lecture Notes in Computer Science 2960 275–359.Google Scholar
Mosses, P. D. (2004) (ed.) Casl Reference Manual. Springer-Verlag Lecture Notes in Computer Science 2960.Google Scholar
Popescu, A. and Roşu, G. (2005) Behavioral extensions of institutions. Proc. 1st Conf. on Algebra and Coalgebra in Computer Science CALCO'05, Swansea. Springer-Verlag Lecture Notes in Computer Science 3629 331–347.CrossRefGoogle Scholar
Reichel, H. (1981) Behavioural equivalence – a unifying concept for initial and final specification methods. Proc. 3rd Hungarian Comp. Sci. Conference 27–39.Google Scholar
Sannella, D. and Tarlecki, A. (1988a) Specifications in an arbitrary institution. Information and Computation 76 165–210.CrossRefGoogle Scholar
Sannella, D. and Tarlecki, A. (1988b) Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25 233–281.CrossRefGoogle Scholar
Sannella, D. and Tarlecki, A. (1989) Toward formal development of ML programs: foundations and methodology. Proc. Colloq. on Current Issues in Programming Languages, Intl. Joint Conf. on Theory and Practice of Software Development TAPSOFT'89, Barcelona. Springer-Verlag Lecture Notes in Computer Science 352 375–389.CrossRefGoogle Scholar
Sannella, D. and Tarlecki, A. (1997) Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9 229–269.CrossRefGoogle Scholar
Schoett, O. (1987) Data Abstraction and the Correctness of Modular Programming, Ph.D. thesis, University of Edinburgh. (Report CST-42-87, Department of Computer Science, University of Edinburgh.)Google Scholar
Schoett, O. (1990) Behavioural correctness of data representations. Science of Computer Programming 14 43–57.CrossRefGoogle Scholar
Schröder, L. and Mossakowski, T. (2002) HasCasl: Towards integrated specification and development of functional programs. Proc. 9th Intl. Conf. on Algebraic Methodology and Software Technology, AMAST'02. Springer-Verlag Lecture Notes in Computer Science 2422 99–116.CrossRefGoogle Scholar
Schröder, L., Mossakowski, T., Tarlecki, A., Hoffman, P. and Klin, B. (2001) Semantics of architectural specifications in Casl. Proc. 4th Intl. Conf. on Fundamental Approaches to Software Engineering FASE'01. Springer-Verlag Lecture Notes in Computer Science 2029 253–268.CrossRefGoogle Scholar
Schröder, L., Mossakowski, T., Tarlecki, A., Hoffman, P. and Klin, B. (2005) Amalgamation in the semantics of Casl. Theoretical Computer Science 331 215–247.CrossRefGoogle Scholar
Szyperski, C. (1998) Component Software: Beyond Object-Oriented Programming, ACM Press and Addison-Wesley.Google Scholar
Tarlecki, A. (2003) Abstract specification theory: An overview. In: Broy, M. and Pizka, M. (eds.) Models, Algebras and Logic of Engineering Software. NATO Science Series – Computer and Systems Sciences, IOS Press 19143–79.Google Scholar