Program transformation using partial functions which preserve partial correctness

Question

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?

Answer 1

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.