Verificación y síntesis de programas funcionales