A. Gammelgaard, “Reuse of Invariants in Proofs of Implementation”, DPB, vol. 20, no. 360, Jul. 1991.