Gammelgaard, A. Reuse of Invariants in Proofs of Implementation. DPB 1991, 20.