Actions that Terminate Exceptionally

Many advanced programming languages support exception handling and thus I should be able to specify the interface of a program that can raise exceptions.

Consider the following Stack machine:

with push and pop specified as follows:

1

 pushĒ(i: int)/ok()

            		pre true

            		post   

pop()/ok(int)

            		pre   

            		post    

Here's how I specify a more robust interface to Stack that allows pop to raise the exception empty if I try to perform the pop action on an empty stack (push stays the same):

1

 pop()Ē/ok(int), empty()

            		pre true

            		post ¯  

                      				   

The first thing to notice is the addition of the name of the exceptional termination condition, empty, in the header. For each termination condition (normal and exceptional), I allow some kind of result to be returned; here empty does not return any result.

The second thing to notice is the special reserved word, terminates, which I introduced to hold the value of the termination condition (``ok'' for normal termination and one of the exceptions listed in the header for an exceptional termination).

From a software engineering perspective, there's usually a close correlation between pre-conditions and exceptions. It's common to transform a ``check'' in the pre-condition to be a ``check'' in the post-condition. From your programming experience, this is the same as placing the responsibility on the callee rather than the caller of a procedure. With a pre-condition it's the caller's responsibility to check that the state of the system satisfies the pre-condition before calling the procedure; with an exception in lieu of the pre-condition, it's the callee's responsibility by performing a (run-time) check and raise an exception in case the state of the system violates the condition.

Here's an example where upon exceptional termination an interesting value is returned. Consider a Table machine, which stores keys and values. The state variable, t, stores the CMU telephone extensions of the 15-671 staff members:

We can model the state of the Table as a function from keys to values . The insert action returns an exception already_in if there already exists a value associated with the key for which you are trying to insert a particular key-value pair, (k, v), and if so, it returns the current value bound to that key, k:

1

 insert(k: keyĒ, v: value)/ok(), already_in(value)

            		pre true

            		post ¯