Abstract
We propose a new algebraic framework for exception handling which is powerful enough to cope with many exception handling features such that recovery, implicit propagation of exceptions, etc. This formalism is capable of treating all the exceptional cases, including the following ones: “intrinsic” exceptions which are related to the underlying data structure (for instance, popping an emptstack or applying predecessor on zero for natural numbers), exceptions which are relied on “dynamic” properties (as an acces to a non-initialized array cell) or else exceptions which are due to certain limitations (mainly bounded data structures). We show that within the already existing frameworks, the case of bounded data structures with certain recoveries of exceptional values remains unsolved.
First, we justify the usefulness of “labelling” some terms in order to easily specify exceptions without inconsistency, and we then define a general framework of label algebras which allows us to “type” terms instead of values. Exception algebras and exception specifications are defined as a direct application of label algebras. Indeed, the usual inconsistency problems raised by exception handling are avoided by the possibility of labelling terms.
As a conclusion, we also sketch out how far the application domain of label algebras seems to be much more general than exception handling.
Chapter PDF
Similar content being viewed by others
Key-words
References
Bernot G., Bidoit M. Proving the correctness of algebraically specified software: Modularity and Observability issues. Proc. of AMAST-2, Second Conference of Algebraic Methodology and Software Technology, Iowa City, Iowa, USA, May 1991.
Bernot G., Bidoit M., Choppy C. Abstract data types with exception handling: an initial approach based on a distinction between exceptions and errors. Theoretical Computer Science, Vol.46, n.1, pp.13–45, Elsevier Science Pub. B.V. (North-Holland), November 1986. (Also LRI Report 251, Orsay, Dec. 1985.)
Bernot G. Une sémantique algébrique pour une spécification différenciée des exceptions et des erreurs: application à l'implémentation et aux primitives de structuration des spécifications formelles. Thèse de troisième cycle, Université de Paris-Sud, Orsay, February 1986.
Bernot G., Le Gall P. Label algebras: a systematic use of terms. “8th International Workshop on Abstract Data Types”, Dourdan, August 1991. LNCS 655 p 144–163. (also LRI Report 719, Orsay, Dec. 1991.)
Bernot G., Le Gall P. Label algebras and exception handling. Draft Version (also in Habilitation Thesis of Bernot G., University of Orsay, Paris XI, Feb. 1992.)
Bidoit M. Algebraic specification of exception handling by means of declarations and equations. Proc. 11th ICALP, Springer-Verlag LNCS 172, July 1984.
Broy M., Wirsing M. Partial abstract data types. Acta Informatica, Vol.18-1, Nov. 1982.
Ehrig H., Mahr B. Fundamentals of Algebraic Specification 1. Equations and initial semantics. EATCS Monographs on Theoretical Computer Science, Vol.6, Springer-Verlag, 1985.
Futatsugi K., Goguen J., Jouannaud J-P., Meseguer J. Principles of OBJ2. Proc. 12th ACM Symp. on Principle of Programming Languages, New Orleans, january 1985.
Gogolla M., Drosten K., Lipeck U., Ehrich H.D. Algebraic and operational semantics of specifications allowing exceptions and errors. Theoretical Computer Science 34, North Holland, 1984, pp.289–313.
Goguen J.A., Meseguer J. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Technical Report SRI-CSL-89-10, SRI, July 1989.
Goguen J.A. Abstract errors for abstract data types. Formal Description of Programming Concepts, E.J. NEUHOLD Ed., North Holland, pp.491–522, 1978.
Goguen J.A. Order sorted algebras: exceptions and error sorts, coercion and overloading operators. Univ. California Los Angeles, Semantics Theory of Computation Report n.14, Dec. 1978.
Goguen J.A., Thatcher J.W., Wagner E.G. An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types. Current Trends in Programming Methodology, ed. R.T. Yeh, Printice-Hall, Vol.IV, pp.80–149, 1978. (Also IBM Report RC 6487, October 1976.)
Guttag J.V. The specification and application to programming. Ph.D. Thesis, University of Toronto, 1975
Hennicker R. Implementation of Parameterized Observational Specifications. TapSoft, Barcelona, LNCS 351, vol.1, pp.290–305, 1989.
Le Gall P. Les algèbres étiquetées: une sémantique fondée sur une utilisation systématique des termes. Application au test de logiciel avec traitement d'exceptions. forthcoming thesis, University of Orsay, 1993.
Liskov B., Zilles S. Specification techniques for data abstractions. IEEE Transactions on Software Engineering, Vol.SE-1 n.1, March 1975.
Mac Lane S. Categories for the working mathematician. Graduate texts in mathematics, 5, Springer-Verlag, 1971
Mégrelis A. Algèbre galactique — Un procédé de calcul formel, relatif aux semi-fonctions, à l'inclusion et à l'égalité. Ph.D. Thesis, University of Nancy I, Sept. 1990.
Mosses P. Unified algebras and Institutions. Proc. of IEEE LICS'89, Fourth Annual Symposium on Logic in Computer Science, June 1989, Asilomar, California.
Manca V., Salibra A. and Scollo G. Equational Type Logic. Conference on Algebraic Methodology and Software Technology, Iowa City, IA, May 1989, TCS 77, p 131–159.
Poigné A. Partial algebras, subsorting, and dependent types Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types, Gullane, Scotland, September 1987. LNCS 332, p 208–234.
Schobbens P.Y. Clean algebraic exceptions with implicit propagation. Proc. of AMAST-2, Second Conference of Algebraic Methodology and Software Technology, Iowa City, Iowa, USA, May 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bernot, G., Le Gall, P. (1993). Exception handling and term labelling. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_80
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_80
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive