When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents and explores this technique in a general setting; it states the lemmas that must be established to use the technique to prove the correctness of a program transformation, and sketches how to apply the technique to slicing of probabilistic programs.

翻译：在证明概率程序切片方法的正确性时，作者先前发现，为了使定点迭代有效，需要为迭代选择一个非标准的起始点。本文在一般性框架下提出并探讨了该技术；文中阐述了使用该技术证明程序变换正确性所需建立的引理，并概述了如何将该技术应用于概率程序的切片。