Semantics-based generation of verification conditions by program specialization