article

Open access

An axiomatic treatment of exception handling in an expression-oriented language

Editor: Susan L. Graham Authors:

Daniel M. BerryAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 9, Issue 3

Pages 390 - 407

https://doi.org/10.1145/24039.24052

Published: 01 July 1987 Publication History

Abstract

An axiomatic semantic definition is given of the replacement model of exception handling in an expression-oriented language. These semantics require only two new proof rules for the most general case. An example is given of a program fragment using this model of exception handling, and these rules are used to verify the consistency of the fragment and its specification.

References

[1]

IBM OS PL/I Checkout and Optimizing Compilers: Language Reference Manual. SC33-0009-2, IBM Corp. (1973).

[2]

Ada Language Reference Manual. MIL-STD-1815A, U.S. Department of Defense (1983).

[3]

BOEHM, H.-J. Side-effects and aliasing can have simple axiomatic descriptions. ACM Trans. Programm. Lang. Sys. 7, 4 (Oct. 1985), 637-655.

[4]

CUNT, M. AND HOARE, C.A.R. Program proving: jumps and functions. Acta Inf. 1 (1972), 214-224.

[5]

COCCO, N. AND DULLI, S. A mechanism for exception handling and its verification rules. J. Comput. Lang. 7 (1982), 89-102.

[6]

CRISP^N, F. Reasoning about programs with exceptions. In Proceedings Thirteenth International Symposium on Fault-Tolerant Computing (Milano, Italy, June 27-30 1983), IEEE, 188-195.

[7]

CRISTIAN, F. Correct and robust programs. IEEE Trans. Softw. Eng. SE-IO, 2 (March 1984).

[8]

D1JKSTRA, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ (1976).

[9]

GO,YEN, J.A. Abstract errors for abstract data types. In Formal Description of Programming Concepts (St. Andrews, N.B., Canada, 1978), North-Holland, Amsterdam, 491-527.

[10]

GOODENOUGH, J.B. Exception handling: issues and a proposed notation. Commun. ACM 18, 2 (Dec. 1975).

[11]

GRIES, D. The Science of Programming. Springer-Verlag, New York (1985).

[12]

HOARE, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576- 580,585.

[13]

HOARE, C.A.R. Procedures and parameters: an axiomatic approach. In Symposium on Semantics of Algorithmic Languages (Minneapolis, MN, 1971), Springer-Verlag, Berlin.

[14]

ICHBIAH, J.D. Rationale for the design of the Ada programming language. SIGPLAN Not. 14, 6 (June 1979).

[15]

KOWALTOWSKI, T. Axiomatic approach to side effects and general jumps. Acta Inf. 7 (1977), 357-360.

[16]

LEVIN, R. Program structures for exceptional condition handling. Ph.D. dissertation, Carnegie Mellon University, Pittsburgh, PA (June 1977).

[17]

LISKOV, B.H. AND SNYDER, A. Structured Exception Handling. Computation Structures Group Memo 155, MIT (Dec. 1977).

[18]

LUCKHAM, D.C. AND POLAK, W. Ada exception handling, an axiomatic approach. ACM Trans. Programm. Lang. Sys. 2, 2 (April 1980), 225-233.

[19]

MITCHELL, J.G., MAYBUR~, W., AND SWEET, R. MESA Language Manual. Xerox Research Center, Palo Alto, CA (March 1979).

[20]

PARNAS, D.L. Response to Detected Errors in Well-Structured Programs. Computer Science Department, Carnegie-Mellon University (1972).

[21]

PNUELI, A. The temporal logic of programs. In Eighteenth Annual Symposium on the Foundations of Computer Science (Providence, RI, Oct. 31-Nov. 2 1977), IEEE, 46-57.

[22]

PmTCHARD, P. Program proving -- expression languages. In Information Processing 1977 (Toronto, Canada, August 2-12 1977), North-Holland, Amsterdam, 727-731.

[23]

SCHWARTZ, R.L. An axiomatic treatment of ALGOL 68 routines. In Proceedings Sixth International Conference on Automata, Languages and Programming (Graz, Austria, July 1979), Springer-Verlag, Berlin, 530-545.

[24]

SCHWARTZ, R.L. An axiomatic semantic definition of ALGOL 68. Ph.D. dissertation, Computer Science Department, UCLA, Los Angeles, CA (1980).

[25]

WIJNGAARDEN, A. VAN, MAILLOUX, B.J., PECK, J.E.L., KOSTER, C.H.A, SINTZOFF, M., LINDSEY, C.H., MEERTENS, L.G.L.T., AND FISKER, R.G. Revised report on the algorithmic language ALGOL 68. Acta Inf. 5, 1-3 (1975), 1-236.

[26]

YEMINI, S. The replacement model for modular verifiable exception handling. Ph.D. dissertation, Computer Science Department, UCLA, Los Angeles, CA (1980).

[27]

YEMINI, S. AND BERRY, D.M. A modular verifiable exception handling mechanism. ACM Trans. Programm. Lang. Sys, 7, 2 (April 1985), 214-243.

Cited By

van Dooren MSteegmans E(2005)Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarationsACM SIGPLAN Notices10.1145/1103845.109484740:10(455-471)Online publication date: 12-Oct-2005
https://dl.acm.org/doi/10.1145/1103845.1094847
van Dooren MSteegmans EJohnson RBaniassad EGabriel RNoble JMarick B(2005)Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarationsProceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications10.1145/1094811.1094847(455-471)Online publication date: 17-Oct-2005
https://dl.acm.org/doi/10.1145/1094811.1094847
Bretz MEbert J(2005)An exception handling construct for functional languagesESOP '8810.1007/3-540-19027-9_11(160-174)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-19027-9_11
Show More Cited By

Index Terms

Recommendations

Ada exception handling: an axiomatic approach

A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications, permitting documentation of those exceptions that can be propagated by a ...
Efficient Java exception handling in just-in-time compilation
Research Articles

Java uses exceptions to provide elegant error handling capabilities during program execution. However, the presence of exception handlers complicates the job of the just-in-time (JIT) compiler, while exceptions are rarely used in most programs. This ...
Data-oriented exception handling

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 9, Issue 3

July 1987

166 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/24039

Editor:
Susan L. Graham

Issue’s Table of Contents

Copyright © 1987 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1987

Published in TOPLAS Volume 9, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
416
Total Downloads

Downloads (Last 12 months)57
Downloads (Last 6 weeks)8

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

van Dooren MSteegmans E(2005)Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarationsACM SIGPLAN Notices10.1145/1103845.109484740:10(455-471)Online publication date: 12-Oct-2005
https://dl.acm.org/doi/10.1145/1103845.1094847
van Dooren MSteegmans EJohnson RBaniassad EGabriel RNoble JMarick B(2005)Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarationsProceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications10.1145/1094811.1094847(455-471)Online publication date: 17-Oct-2005
https://dl.acm.org/doi/10.1145/1094811.1094847
Bretz MEbert J(2005)An exception handling construct for functional languagesESOP '8810.1007/3-540-19027-9_11(160-174)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-19027-9_11
Govindarajan R(1993)Exception Handlers in Functional Programming LanguagesIEEE Transactions on Software Engineering10.1109/32.23858519:8(826-834)Online publication date: 1-Aug-1993
https://dl.acm.org/doi/10.1109/32.238585
Guaspari DMarceau CPolak W(1993)Formal Verification of Ada ProgramsFirst International Workshop on Larch10.1007/978-1-4471-3558-6_8(104-141)Online publication date: 1993
https://doi.org/10.1007/978-1-4471-3558-6_8
Shih TDavis RLin F(1993)Disciplined Exceptions in Logic ProgrammingALPUK9210.1007/978-1-4471-3421-3_8(124-141)Online publication date: 1993
https://doi.org/10.1007/978-1-4471-3421-3_8
Govindarajan R(1992)Software fault-tolerance in functional programming[1992] Proceedings. The Sixteenth Annual International Computer Software and Applications Conference10.1109/CMPSAC.1992.217569(194-199)Online publication date: 1992
https://doi.org/10.1109/CMPSAC.1992.217569
Gehani N(1992)Exceptional C or C with exceptionsSoftware—Practice & Experience10.1002/spe.438022100322:10(827-848)Online publication date: 1-Oct-1992
https://dl.acm.org/doi/10.1002/spe.4380221003
Issarny VMoriconi M(1991)An exception handling model for parallel programming and its verificationProceedings of the conference on Software for citical systems10.1145/125083.123058(92-100)Online publication date: 1-Sep-1991
https://dl.acm.org/doi/10.1145/125083.123058
Issarny V(1991)An exception handling model for parallel programming and its verificationACM SIGSOFT Software Engineering Notes10.1145/123041.12305816:5(92-100)Online publication date: 1-Sep-1991
https://dl.acm.org/doi/10.1145/123041.123058
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents