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?
I imagine that you can prove this straight from the operational
semantics using the standard operational precongruence (assuming that
you have a sequential language). Some of the relevant techniques
have been collected in Operationally-based theories of program equivalence by
Andy Pitts.

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.

Such questions come up all the time in proving observational and
descriptive completeness of Hoare logics. As Neel points out in 
an answer to your other question, domain theory is based upon
related ideas.