Abstract
OBSCURE is a specification language for abstract data types. It differs from classical specification languages by handling models rather than theories. The goal of the paper is to present a complete and precise description ofOBSCURE.
First, the different language constructs are illustrated by the help of examples. The syntax and semantics of the language are then defined formally. The consistency of these definitions is stated in two theorems. Next, a set of formulas is associated with each specification. A further theorem states that these formulas guarantee the persistency or, more precisely, the absence of logical inconsistencies. A discussion of further language concepts-such as parameterization and strong typing-follows. Finally, a methodology for the development of software with the help ofOBSCURE is sketched and some practical results are presented.
Similar content being viewed by others
References
Bergstra, J.A., Heering, J., Klint, P.: Algebraic specification. New York: ACM-Press 1989
Bidoit, M.: PLUSS, a language for the development of modular algebraic specifications. Thèse d'Etat, Université Paris-Sud, 1989
Bidoit, M., Gaudel, M.-C., Mauboussin, A.: How to make algebraic specifications more understandable: An experiment with the PLUSS specification language. Sci. Comput. Programm.12(1), 1–38 (1989)
Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., Sannella, D. (Eds.): Algebraic system specification and development. (Lect. Notes Comput. Sci., Vol. 501) Berlin Heidelberg New York: Springer 1991
Broy, M. et al.: The requirement and design specification language SPECTRUM. Internal Report, Techn. Univ. München (May 1992)
Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification language. In: Proc. 1979 Copenhagen Winter School. (Lect. Notes Comput. Sci., Vol. 86, pp. 292–332) Berlin Heidelberg New York: Springer 1980
Cartwright, R.: A constructive alternative to abstract data type definitions. In: Proc. 1980 LISP Conf., Stanford Univ., pp. 46–55 (1980).
Dollin, Ch., Arnold, P., Coleman, D., Gilchrist, H., Rush, T.: Axis tutorial: a simple filing system. Internal Report HPL-ISC-TM-88-18, Hewlet-Packard Ltd., Bristol (1988).
Ehrich, H.D., Gogolla, M., Lipeck, U.: Algebraische Spezifikation abstrakter Datentypen. Stuttgart: Teubner 1989
Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1-equations and initial semantics. Berlin Heidelberg New York: Springer 1985
Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 2-module specifications and constraints. Berlin Heidelberg New York: Springer 1990
Fey, W.: Pragmatics, concepts, syntax, semantics and correctness notions of ACT TWO: An algebraic module specification and interconnection language. Internal report 1988/26, TU Berlin, 1988
Fuchs, J., Hoffmann, A., Meiss, L., Philippi, J., Stolz, M., Wolf, M., Zeyer, J.: The OBSCURE manual. Part 1: Editing and rapid prototyping. Internal Report, Universität Saarbrücken (1991)
Goguen, J.A., Winkler, T.: Introducing OBJ3. Int. Rep. SRI-CSL-88-9. Comput. Sci. Laboratory SRI International. 1988
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J.ACM39 (1), 95–146 (1992)
Heckler, R., Loeckx, J., Uhrig, St.: Ein Fallbeispiel: Das Dateisystem von UNIX. Internal Report WP 91/30. Universität Saarbrücken (1991)
Ayari, A., Friedrich, S., Heckler, R., Loeckx, J.: Das Fallbeispiel LEX. Internal Report WP92/39, Universität Saarbrücken (December 1992)
Hettler, R.: Spezifikation eines LEX-artigen Scanners. Eine SPECTRUM Fallstudie. Internal Report, TU München (November 1992)
Klaeren, H.A.: A constructive method for abstract algebraic software specification. Theor. Comput. Sci.30, 139–204 (1984)
Krieg-Brückner, B.: Algebraic formalisation of program development by transformation. In: Ganzinger H. (ed.) Proc. ESOP 88. (Lect. Notes Comput. Sci., Vol. 300) Berlin Heidelberg New York: Springer 1988
Krieg-Brückner, B., Sannella, D.: Structuring specifications in-the-large and in-the-small: Higher-order functions, dependent types and inheritance in SPECTRAL. Proceedings TAPSOFT 91. (Lect. Notes Comput. Sci., Vol. 494, pp. 313–336) Berlin Heidelberg New York: Springer 1991
Lehmann, T.: A notion of implementation of the specification language OBSCURE, Proc. Workshop on Abstract Data Types (Wusterhausen). (Lect. Notes Comput. Sci., Vol. 534, pp. 141–165) Berlin Heidelberg New York: Springer 1991
Lehmann, T., Loeckx, J.: The specification language of OBSCURE. In: Sannella, D., Tarlecki, A. (eds.), Proc. of the 5th Workshop on Specification of Abstract Data Types. (Lect. Notes Comput. Sci., Vol. 332, pp. 131–153) Berlin Heidelberg New York: Springer 1988
Loeckx, J.: Algorithmic specifications: a constructive specification method for abstract data types. ACM Trans. Program. Lang. Syst.9, 646–685 (1987)
Loeckx, J.: The specification system OBSCURE. Bull. EATCS40, 169–171 (1990)
Loeckx, J., Zeyer, J.: A calculus for OBSCURE. Internal Report (to appear)
Milner, R.: Logic for computable functions: description of a machine implementation. SIGPLAN NOTICES7, 1–6 (1972)
Milner, R., Tofte, M., Harper, R.: The definition of standard ML. Cambridge, MA: MIT Press 1990
Partsch, H.: Specification and transformation of programs. Berlin Heidelberg New York: Springer 1990
Sannella, D.: A set-theoretic semantics of CLEAR. Acta Inf.21, 443–472 (1984)
Sannella, D., Tarlecki, A.: Extended ML: past, present and future. Proc. Workshop on Abstract Data Types (Wusterhausen). (Lect. Notes Comput. Sci., Vol. 534, pp. 297–322) Berlin Heidelberg New York: Springer 1991
Sannella, D., Sokolowski, S., Tarlecki, A.: Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Inf.29, 689–736 (1992)
Sannella, D., Tarlecki, A.: Toward formal development of ML programs: foundations and methodology. In: Diaz, J., Orejas, F. (eds.) Proc. of TAPSOFT'89. (Lect. Notes Comput. Sci., Vol. 352, pp. 375–389) Berlin Heidelberg New York: Springer 1989
Turner, D.A.: Miranda: a non-strict functional language with polymorphic types. In: Goos, G., Hartmanis, J. (eds.) Functional programming and computer architecture. (Lect. Notes Comput. Sci., Vol. 201, pp. 1–16) Berlin Heidelberg New York: Springer 1985
Walther, Chr.: Automated termination proofs. Internal Report 17/88, Universität Karlsruhe (1988)
Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.) Handbook of theoretical computer science. Amsterdam: North-Holland 1990.
Wirsing, M.: Structured algebraic specifications: a kernel language. Theor. Comput. Sci.42, 124–249 (1986)
Zeyer, J.: Erweiterung des OBSCURE-Systems. Internal Report WP 92/31, Universität Saarbrücken (1992)
Author information
Authors and Affiliations
Additional information
Research supported by the Deutsche Forschungsgemeinschaft (DFG).
Rights and permissions
About this article
Cite this article
Lehmann, T., Loeckx, J. OBSCURE a specification language for abstract data types. Acta Informatica 30, 303–350 (1993). https://doi.org/10.1007/BF01209709
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01209709