A formal framework for synthesis and verification of logic programs