Verificación y derivación formal de programas funcionales