A Formal Framework for Synthesis and Verification of Logic Programs