Verificación de evaluate S11834

Considera la siguiente función:

/* @pre  t és un arbre no buit que representa una expressió 
 *       aritmètica correcta sobre els naturals i 
 *       els operadors +, -, *.
 * @post Retorna l'avaluació de l'expressió representada per t.
 */
int evaluate(BinTree<string> t) {
    int eval = 0;
    if (isNumber(t.value())) {
        eval = mystoi(t.value());
    } else {
        int auxl = evaluate(t.left());
        int auxr = evaluate(t.right());
        if (t.value() == "+") {
            eval = auxl + auxr;
        } else if (t.value() == "-") {
            eval = auxl - auxr;
        } else if (t.value() == "*") {
            eval = auxl * auxr;
        }
    }
    return eval;
}

Recuerda que la función isNumber devuelve un booleano según si el string de entrada representa un entero o no. La función mystoi convierte un string que representa un entero, en un entero.

Pregunta 1
Demuestra que el caso básico es correcto. Es decir, demuestra que si el árbol de entrada cumple la precondición y también la condición isNumber(t.value()) del if, entonces el resultado que se devuelve cumple la poscondición.

Pregunta 2
Escribe las hipótesis de inducción (HI) para el caso recursivo.

Pregunta 3
Demuestra la corrección del algoritmo en el caso en que el árbol de entrada t tenga en la raiz el símbolo +, - o *, usando la HI.

Pregunta 4
Demuestra que el algoritmo acaba. Da una función de cota y muestra sus propiedades.

Observación

El fichero a enviar debe ser un .tar dentro del cual haya un fichero de texto respuestas.txt con las respuestas a las preguntas. (El veredicto del Jutge siempre será verde, porque las respuestas se evaluarán manualmente.)