We present a new way to define the semantics of imperative synchronous languages by means of separating the control and the dataflow. The control flow is defined by predicates that describe entering conditions, conditions for internal moves, and termination conditions. The dataflow is based on the extraction of guarded commands. This definition principle can be applied to any imperative synchronous language like Esterel or some statechart variants. Following this definition principle, we have embedded our language Quartz (an Esterel variant) in the interactive theorem prover HOL We use this embedding for formal verification (both interactive theorem proving and symbolic model checking), program analysis, reasoning about the language at a meta-level, and verified code generation (formal synthesis).