zeno is not just another exception handling technique - rather it is a design paradigm that enforces the proper specification and implementation of exceptional circumstances. It is a lot like object oriented programming: the object oriented programming paradigm can be used on any progrmaming language. Smalltalk was not developed until it became clear that object oriented approaches would work using existing languages. Anyway, I am getting off base here. possible experiments: 1. Use the total function model on a small class that you have such as strings or vectors. See what it buys you. 2. Use the total function model at the highest level of a design - such as the control display. Does it buy you anything? Are there problems posed by interfacing with existing code? 3. How would one exploit existing (C++) exception handling in a total-function program? Sketch a rudimentary translation between the concepts of total-functions and C++ constructs. 4. Do the same thing for C, given that it has no exceptions. Can you sketch a pre-processor that would add a hidden exception parameter? [in both of these cases, you don't need a complete proof, just convince the reader that it will work and that you have considered the sticky points] 5. Reconcile what you have said with Hoare's opinion that exceptions should not be used. Show that your stuff is actually a generalization of Hoare's thinking. precondition free? free at level of needing to consider them without seeing them, but they are still there in the underlying model. the verification system will rely heavily on computed preconditions. there are two senses of precondition: one is in the sense of conditions that you have to ensure before you invoke an operation (because otherwise the operation is not defined). the other sense is what conditions have been established by prior operations when a particular operation is invoked. this is a computed thing, and this is the sense that zeno will deal with preconds in. the other is given a different slant in that you need now to consider which segment of the operand space is what you're interested in. names can help you clue in (overflow versus sum). the domain specification helps you clue in the most precisely. but now you just connect at will and let the verifier help you to making it stick in the right way. you don't have to ensure a condition, rather you rely on paths? blurph.