A language-based approach to functionally correct imperative programming