zbMATH — the first resource for mathematics

OBSCURE, a specification language for abstract data types. (English) Zbl 0790.68072
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 of OBSCURE.
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 of OBSCURE is sketched and some practical results are presented.
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification
68N15 Theory of programming languages
Full Text: DOI
[1] Bergstra, J.A., Heering, J., Klint, P.: Algebraic specification. New York: ACM-Press 1989 · Zbl 0711.68073
[2] Bidoit, M.: PLUSS, a language for the development of modular algebraic specifications. Th?se d’Etat, Universit? Paris-Sud, 1989
[3] 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) · Zbl 0678.68011 · doi:10.1016/0167-6423(89)90026-9
[4] 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 · Zbl 0875.68642
[5] Broy, M. et al.: The requirement and design specification language SPECTRUM. Internal Report, Techn. Univ. M?nchen (May 1992)
[6] 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 · Zbl 0456.68024
[7] Cartwright, R.: A constructive alternative to abstract data type definitions. In: Proc. 1980 LISP Conf., Stanford Univ., pp. 46-55 (1980).
[8] 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).
[9] Ehrich, H.D., Gogolla, M., Lipeck, U.: Algebraische Spezifikation abstrakter Datentypen. Stuttgart: Teubner 1989 · Zbl 0696.68011
[10] Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1-equations and initial semantics. Berlin Heidelberg New York: Springer 1985 · Zbl 0557.68013
[11] Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 2-module specifications and constraints. Berlin Heidelberg New York: Springer 1990 · Zbl 0759.68013
[12] 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 · Zbl 1086.68521
[13] 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)
[14] Goguen, J.A., Winkler, T.: Introducing OBJ3. Int. Rep. SRI-CSL-88-9. Comput. Sci. Laboratory SRI International. 1988
[15] Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J.ACM39 (1), 95-146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524
[16] Heckler, R., Loeckx, J., Uhrig, St.: Ein Fallbeispiel: Das Dateisystem von UNIX. Internal Report WP 91/30. Universit?t Saarbr?cken (1991)
[17] Ayari, A., Friedrich, S., Heckler, R., Loeckx, J.: Das Fallbeispiel LEX. Internal Report WP92/39, Universit?t Saarbr?cken (December 1992)
[18] Hettler, R.: Spezifikation eines LEX-artigen Scanners. Eine SPECTRUM Fallstudie. Internal Report, TU M?nchen (November 1992)
[19] Klaeren, H.A.: A constructive method for abstract algebraic software specification. Theor. Comput. Sci.30, 139-204 (1984) · Zbl 0544.68016 · doi:10.1016/0304-3975(84)90062-8
[20] 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
[21] 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
[22] 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
[23] 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 · Zbl 0663.68024
[24] Loeckx, J.: Algorithmic specifications: a constructive specification method for abstract data types. ACM Trans. Program. Lang. Syst.9, 646-685 (1987) · Zbl 0631.68020 · doi:10.1145/29873.30399
[25] Loeckx, J.: The specification system OBSCURE. Bull. EATCS40, 169-171 (1990) · Zbl 0744.68101
[26] Loeckx, J., Zeyer, J.: A calculus for OBSCURE. Internal Report (to appear)
[27] Milner, R.: Logic for computable functions: description of a machine implementation. SIGPLAN NOTICES7, 1-6 (1972) · doi:10.1145/942578.807067
[28] Milner, R., Tofte, M., Harper, R.: The definition of standard ML. Cambridge, MA: MIT Press 1990
[29] Partsch, H.: Specification and transformation of programs. Berlin Heidelberg New York: Springer 1990 · Zbl 0751.68036
[30] Sannella, D.: A set-theoretic semantics of CLEAR. Acta Inf.21, 443-472 (1984) · Zbl 0545.68075 · doi:10.1007/BF00271641
[31] 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
[32] Sannella, D., Sokolowski, S., Tarlecki, A.: Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Inf.29, 689-736 (1992) · Zbl 0790.68077 · doi:10.1007/BF01191893
[33] 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
[34] 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 · Zbl 0592.68014
[35] Walther, Chr.: Automated termination proofs. Internal Report 17/88, Universit?t Karlsruhe (1988) · Zbl 0656.68104
[36] Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.) Handbook of theoretical computer science. Amsterdam: North-Holland 1990. · Zbl 0900.68309
[37] Wirsing, M.: Structured algebraic specifications: a kernel language. Theor. Comput. Sci.42, 124-249 (1986) · Zbl 0599.68021 · doi:10.1016/0304-3975(86)90051-4
[38] Zeyer, J.: Erweiterung des OBSCURE-Systems. Internal Report WP 92/31, Universit?t Saarbr?cken (1992)
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.