Abstract Correction of First-Order Functional Programs