Dynamic linking supports flexible code deployment: partially linked
code links further code on the fly, as needed; and thus, end-users
receive updates automatically. On the down side, each program run may
link different versions of the same code, a powerful feature possibly
causing subtle errors which mystify end-users.
Dynamic linking in Java and C# are similar: the same linking phases
are involved, soundness is based on similar ideas, and executions
which do not throw linking errors of programs in the intersection of
the languages give the same result. They are, however, not identical:
the linking phases in Java and C# are combined differently, and take
place in a different order. Thus, linking errors may be detected at
different times in Java and C#.
We develop a non-deterministic model, which includes the behaviour of
Java and C#. The non-determinism allows us to describe the design
space, to distill the similarities between the two languages, and to
use one proof of soundness for both. We prove soundness by means of a
subject reduction theorem, and also prove that all execution
strategies are equivalent in the sense that all terminating executions
which do not involve a link error, give the same result.