Synthesis of nonlinear continuous controllers for verifiably correct high-level, reactive behaviors