<p>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 <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.137.4615&amp;rep=rep1&amp;type=pdf" rel="nofollow">Operationally-based theories of program equivalence</a> by
Andy Pitts.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-10-14T21:08:45.873Z
2013-10-14T21:08:45.873Z
Martin Berger
<p>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$.</p>

<p>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.</p>

<p>Can anyone help me out? A reference, a proof, a different formalism?</p>

<lo.logic><turing-machines><program-verification>
Program transformation using partial functions which preserve partial correctness
Jodag
# Program transformation using partial functions which preserve partial correctness

(Asked by: username_0 on 2013-10-14)

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?

**Tags:** lo.logic, turing-machines, program-verification

---

## 1 answers

### Answer by username_1 on 2013-10-14. Score: 3 | Accepted answer

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](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.137.4615&rep=rep1&type=pdf) 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.


---

