Program transformation using partial functions which preserve partial correctness
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.