An Imperative Language for Verified Exact Real-Number Computation