In the next few days and weeks, I'm going to send out some examples of "use cases" for BitC. For many of these, what I'm really trying to figure out is whether there is a simpler approach than full verification. I'm particularly interested in suggestions on how to model these properties, and also how to capture them. shap