The latest (August 2012) issue of Communications ACM, the main magazine of ACM, one of the main Computer Science organizations, has an article "Continuity and Robustness of Programs". This article describes techniques that, based on a step-by-step description of an algorithm as a sequence of steps, proves that the resulting functions is continuous -- exactly one of the objectives of using decorations.
The algorithms presented in this paper go beyond proving continuity, to proving that the resulting function is Lipschitz-continuous, and to computing the corresponding Lipschitz constant.