The safety of dynamic mixin composition

Dynamic mixins are a modular means of developing features or roles that can be composed with objects at run-time. However, naive use of this construct can cause unexpected behaviour due to interference caused by the presence of an object's previously bound mixins. This work proposes a method for developing mixins that can be bound to base objects such that the mixins do not interfere with each other; the method achieves compositionally through a coupling invariant and by syntactically restricting mixins. The refinement calculus is used for formalization, as it treats implementations and specifications uniformly. The formalization relies on a new notion of mixin refinement.