While exceptions can be very useful in practice, it is also very common to see code that misuses exceptions.
Generally speaking, there are exceptions that are meant to be raised but not captured for the purpose of aborting program execution, and there are also exceptions (often declared locally) that are meant to be raised and then captured so as to change the flow of program execution. For instance, the exception ArraySubscriptExn is raised when out-of-bounds array subscripting is detected at run-time. Once it is raised, ArraySubscriptExn is usually not meant to be captured. While there is certainly nothing preventing a programer from writing code that captures a raised ArraySubscriptExn, a major concern is that reasoning can become greatly complicated on code that does so. In the following presentation, I will soley focus on exceptions that are meant to be raised and then captured.
Let us now take a look at the following code that implements a function for finding the rightmost element in a list that satisfies a given predicate:
extern fun{a:t@ype} list_find_rightmost (List (a), (a) -<cloref1> bool): Option_vt (a) // implement{a} list_find_rightmost (xs, pred) = let // fun aux ( xs: List(a) ) : Option_vt (a) = case+ xs of | nil () => None_vt () | cons (x, xs) => let val res = aux (xs) in case+ res of | Some_vt _ => res | ~None_vt () => if pred (x) then Some_vt (x) else None_vt () // end of [None] end (* end of [cons] *) // in aux (xs) end // end of [list_find_rightmost]
implement{a} list_find_rightmost (xs, pred) = let // exception Found of (a) // fun aux ( xs: List(a) ) : void = case+ xs of | nil () => () | cons (x, xs) => let val () = aux (xs) in if pred (x) then $raise Found(x) else () end (* end of [cons] *) // in // try let val () = aux (xs) in None_vt () end with | ~Found(x) => Some_vt (x) // end // end of [list_find_rightmost]
The implementation of the run-time support for exceptions in ATS makes use of the function alloca declared in alloca.h and the functions setjmp and longjmp declared in setjmp.h. If gcc or clang is used to compile the C code generated from ATS source, one can pass the flag -D_GNU_SOURCE so as to make sure that the header file alloca.h is properly included.
Please find on-line the entirety of the code used in this chapter.