hola Franco, qué tal?
sobre lo primero, la respuesta es depende. según el problema y lo que se espere del alg será la prueba de correctitud (que en gral incluye implicitamente probar que el alg termina).
p.e. El ej.3.2 de K&T. pide escribir un alg que detecte ciclos en un grafo, devolviendo uno cuando exista.
si pensamos en una representación para un ciclo, podríamos considerar el uso de una lista simple. en ese caso, nuestro algoritmo devolvería null si no hay ciclo en G o una lista de vértices que sean un ciclo en G en caso contrario.
luego nuestro alg es correcto si, cuando existe ciclo en G (al menos uno) retorna una lista que representa a uno de los ciclos existentes y si cuando no existe ninguno, retorna null.
estos enunciados cubren todos los casos posibles así que alcanza con probar ambos enunciados.
notar que también podríamos probar correctitud si demostramos que, cuando existe ciclo en G el alg retorna un ciclo y que, cuando retorna un ciclo es porque existía uno en G (sii).
por qué es cierto esto. porque este segundo enunciado (recíproco: retorna un ciclo si existía uno en G) es el contra-recíproco del segundo de los enunciados anteriores (recíproco anterior: cuando no existe ninguno, retorna null).
de hecho, utilizar el contra-recíproco del enunciado que queremos probar es una estrategia bastante usual ya que podría ser más fácil de demostrar que el enunciado original.
por último, como decía al comienzo, cada alg tiene un cometido y la correctitud está asociada al resultado esperado, que cambia en cada caso.
sobre lo segundo, diría que es inevitable referirse a la implementación concreta cuando intervienen representaciones de datos estructurados en la solución (algoritmo).
respecto al alg en sí, podría ser un pseudocódigo más o menos cercano a un lenguaje de programación. la clave es que los pasos no sean ambiguos (esté claro como se ejecuta, qué se hace en cada paso)
saludos
