Exceptions are named records of basic values. They can be used only by messages to signal exceptional conditions. The record fields (members) can be used to give more information about the error that caused it. It is desirable to name an exception in such a way as it reflects the kind of error that it is supposed to indicate.
In specifications, checks can be made to see the presence of exceptions using the raised expression. A raised(e) expression evaluates to true after a message m iff m terminates raising the exception e. Expressions can use values of the data members of an exception for writing specifications.