Similar a lo que ocurre con los algoritmos, como ya vimos desde la T01, normalmente, hay muchísimos programas posibles para un mismo algoritmo. Para los fines prácticos de esta clase, para lo que queda de ella, usemos el programa presentado por la cátedra (el que figura en la imagen).

Demostrar que el ciclo en cuestión termina para cualquier entrada válida.

Consejo: aprovechen los casos que vimos; por ejemplo, en la T08.

Escribir un predicado invariante para el ciclo en cuestión, que generalice las descripciones hechas en el ejercicio anterior (disponibles en la imagen) para cualquier valor del string de entrada s y que siga la siguiente estructura "Inv: res vale <completar>".

Consejo 1: recuerden que el predicado invariante debe ser cierto cuando j vale 0; 1; 2; etc.

Consejo 2: aprovechen los casos que vimos; por ejemplo, en la T08.

Consejo 3: aprovechen la cláusula Devuelve de la especificación.

Usar el predicado invariante antes establecido (el que aparece en la imagen) para mostrar que, para cualquier valor del string de entrada s, la función devuelve el valor indicado en la especificación (la suma de los dígitos de s).

Consejo 1: aprovechen los casos que vimos; por ejemplo, en la T08.

Consejo 2: recuerden que, como vimos al resolver el ejercicio 3, el ciclo termina cuando j vale len(s).