update & override: notation and axiomatization

[Jasper Berendsen]

Recently we have published an article titled "The axiomatization of
override and update", which may be of great interest to the Z-community,
since the operators override and update seem to be very important in
Z. Part of the abstract is written below. I am greatly anticipating
reactions on the usefulness/uselessness of our work in Z.

kind regards,
Jasper Berendsen

The axiomatization of override and update
Jasper Berendsen, David N. Jansen, Julien Schmaltz, Frits W. Vaandrager
http://www.elsevier.com/locate/jal
http://dx.doi.org/10.1016/j.jal.2009.11.001

There are only very few natural ways in which arbitrary functions can be
combined. One composition operator is override: for arbitrary functions
f and g, f |> g is the function with domain dom(f) \cup dom(g) that
behaves like f on dom(f) and like g on dom(g) \ dom(f). Another operator
is update: f[g] has the same domain as f, behaves like f on dom(f) \
dom(g), and like g on dom(f) \cap dom(g). These operators are widely
used, especially within computer science, where for instance f[g] may
denote the new state that results when in state f the updates given as g
are applied. It is therefore surprising that thus far no axiomatization
of these operators has been proposed in the literature.