Correct-by-construction code generation from hybrid automata specification