Conference
Verification Rules for Exception Handling in Eiffel
Abstract
The Eiffel exception mechanism supports two methodological aspects. First, a method specification by a pre- and postcondition also determines when the method exits exceptionally, namely when the stated postcondition cannot be satisfied. Secondly, the rescue and retry statements combine catching an exception with a loop structure, thus requiring a dedicated form of correctness reasoning. We present verification rules for total correctness that …
Authors
Sekerinski E; Zhang T
Series
Lecture Notes in Computer Science
Volume
7498
Pagination
pp. 179-193
Publisher
Springer Nature
Publication Date
2012
DOI
10.1007/978-3-642-33296-8_14
Conference proceedings
Lecture Notes in Computer Science
ISSN
0302-9743