We develop within higher order logic (HOL) a general and flexible method of abstraction and refinement, which specifically addresses the problem of handling constraints. The method is based on an interpretation of first-order Lax Logic in HOL, which can be seen as a modal extension of deliverables. It provides a new technique for automating reasoning about behavioural constraints. We show how the method can be applied in several different tasks, for example to achieve a formal separation of the logical and timing aspects of hardware design, and to generate systematically timing constraints for a simple sequential device from a formal proof of its abstract behaviour. The method and all proofs in the paper have been implemented in Isabelle as a definitional extension of the HOL logic. We assume the reader is familiar with higher order logic but do not assume detailed knowledge of circuit design.