# Program transformation using partial functions which preserve partial correctness

Much work has been done demonstrating that certain program transformations preserve particular properties. That is, for any program $P$ which has property $\alpha$, show that $P$ transformed under transformation $T$ still has property $\alpha$.

I'm interested in a transformation which replaces every usage of function $f$ in $P$ with partial function $g$, where $g$ is a restriction of $f$ (meaning that $g(x) = y \implies f(x) = y$). It seems intuitively obvious that this transformation, while not necessarily preserving totatlity, preserves partial correctness. Yet I cannot find a standard proof or reference on this or even mention of this seemingly elemental fact.

Can anyone help me out? A reference, a proof, a different formalism?

If you have a Hoare logic of partial correctness for the language you are interested in, you can probably establish a meta-theorem to the effect that for all programs $M$, all models $\xi, \xi'$ such that $\xi$ is less defined than $\xi'$, and all formulae $A, B$, we have $\xi \models \{A\} M \{B\}$ implies $\xi' \models\{A\} M \{B\}$. Proving such a meta-theorem typically boils down to the operational reasoning mentioned above.