Exceptions

An exception is a control mechanism that allows the programmer to abort the execution of one phrase and start the execution of another.

To demonstrate the use and semantic definition of exceptions we'll introduce them to the language IMP. We do this with a new set of identifiers used only in exceptions:

	  
{exc0,exc1,...}
	  
	

We will represent these identifiers with the generic name exc. We also add two new program phrases:

	
raise exc
exception exc in p1 orelse p2
	
      

In the second phrase, any call of raise exc in p1 would abort the execution and start executing p2. The identifier exc is local to p1.

For the semantic definition we extend the relational semantics definition of IMP. We first change the set Results so that a program may evaluate to a memory or an exception identifier and a memory, i.e. we can have p,M⇒M' or p,M⇒exc,M'. With that done that we move on to give the rules for exceptions.

The raising of an exception is quite simple.

Programs
Raise	raise exc,M ⇒ exc,M

For each program phrase which is a composite containing other program phrases, we introduce rules which allow the aborting of execution of the sub-phrases. As an example, for the sequence phrase we add the following new rules to the existing ones:

Programs
Sequence	p1,M ⇒ exc,M' ------------------- (p1;p2),M ⇒ exc,M' p1,M ⇒ M' p2,M' ⇒ exc,M'' ------------------------    (p1;p2),M ⇒ exc,M''

Finally we add the rules for the exception handling. Note the need for case (3) below where the raised exception does not match that which is handled.

Programs
Exception	p1,M ⇒ M' ------------------------------------ exception exc in p1 orelse p2,M ⇒ M'       p1,M ⇒ exc, M' p2,M' ⇒ M'' ------------------------------------- exception exc in p1 orelse p2,M ⇒ M''          p1,M ⇒ exc', M' -------------------------------------------------------- exception exc in p1 orelse p2,M ⇒ exc',M' where exc'≠exc

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.