Contract-based requirement modularization via synthesis of correct decompositions