Transaction Calculus (Invited Paper)
Jifeng He · Unifying Theories of Programming · 2008
Transaction-based services are increasingly being applied in solving many universal interoperability problems. Compensation is one typical feature for long-running transactions. This paper presents a de- sign model for specifying the behaviour of compensable programs. The new model for handling exception and compensation is built as conserva- tive extension of the standard relational model. The paper puts forward a mathematical framework for transactions where a transaction is treated as a mapping from its environment to compensable programs. We pro- pose a transaction refinement calculus, and show that every transaction can be converted to a primitive one which simply consists of a forward activity and a compensation module.