Formalizing correctness criteria of dynamic updates derived from specification changes.