/*
 * tStart == tryOffset
 * tEnd   == tryOffset + tryLength
 * hStart == handlerOffset
 * hEnd   == handlerOffset + handlerLength
 * in     == index in input
 * out    == index in output
 *
 * E      == "there exists" (existential)
 * A      == "for all" (universal)
 * []     == "such that" section
 * <=>    == comparison operator (always -1, 0, or 1 ... convenient shorthand)
 */

// ok to have no exceptions
!E(e in exceptions)
{}

||

// if we have exceptions, enforce the rules
A(e in exceptions)
{
	// maintain ordering of handlers for a try block (impl. requirement)
	!E(x in exceptions)
	[
		((e.tStart == x.tStart) && (e.tEnd == x.tEnd)) &&
		((e.in <=> x.in) != (e.out <=> x.out))
	]
	{}

	&&

	// ensure inside out ordering for nested try blocks (impl. requirement)
	!E(x in exceptions)
	[
		((e.tStart <= x.tStart) && (e.tEnd >= x.tEnd)) &&
		((e.tStart != x.tStart) || (e.tEnd != x.tEnd)) &&
		(e.out <= x.out)
	]
	{}

	&&

	// ensure proper ordering for remaining exceptions (impl. requirement)
	!E(x in exceptions)
	[
		((e.tStart > x.tStart) && (e.tEnd > x.tEnd)) &&
		(e.out <= x.out)
	]
	{}

	&&

	// ensure well-formed exceptions (verification requirement)
	!E(x in exceptions)
	[
		// is try after handler allowed? if not, TODO line should be changed
		(e == x) &&
		(((e.tStart < x.hStart) && (e.tEnd > x.hStart)) ||
		 ((e.tStart > x.hStart) && (e.tEnd < x.hStart)) || // TODO
		 (e.tStart >= x.tEnd) ||
		 (e.hStart >= x.hEnd) ||
		 (e.tStart == x.hStart))
	]
	{}
}