29_5_Correttezza

//PRE=(albero(r)ben formato, P ha dimP elementi con dimP>0)
nodo* match(nodoA*r, int*P, int dimP){

    if(!r)//Caso base: Albero vuoto non ha match
        return 0;

    nodo* sx = match(r->left,P+1,dimP-1);
    nodo* dx = match(r->right,P+1,dimP-1);

    if(*P == r->info)
        if(dimP == 1)
            return new nodo(r,0); //Caso base --> 1 solo nodo da matchare e l'ho appena matchato
        else
        if(sx)
            return new nodo(r,sx);
        else
            if(dx)
                return new nodo(r,dx);

   //Se sono qui --> No match
   sx = match(r->left,P,dimP);
   dx = match(r->right,P,dimP);

   if(sx)
    return sx;
   else
    if(dx)
      return dx;


    return 0; //Ritorna 0 se non c'è un match completo del pattern. Se arrivo qui --> non c'è match ne a sx ne a dx
}
//POST=(se esiste su un cammino di albero(r)un match di P,allora, restituisce una lista concatenata con dimP nodi ciascuno dei quali punta ad un nodo di albero(r) che partecipa al matchtrovato) &&(altrimenti restituisce 0)


/* -- PROVA INDUTTIVA --

//CASI BASE

1) if(!r) return 0;
    Che è corretto dato che non esiste un match tra una lista e un albero vuoto

2)if(dimP == 1 && r->info == *P) return new nodo(r,0);
    CHe è corretto dato che il pattern contiene solo un'elemento e l'ho appena trovato se sono in questo caso, Ritorno quindi un singolo nodo

//CASI INDUTTIVI

1)
    if(match(r->left,P+1,dimP-1) && r->info == *P) return new nodo(r,match(r->left,P+1,dimP-1)
        Sto matchando un elemento, e il prossimo match è a sinistra, quindi creo un nodo che ha come info il nodo corrente e come next il prossimo match che sarà a sx
    //PRE_ric=(albero(r->left)ben formato, P+1 ha dimP-1 elementi con dimP>1)

        Pre_ric --> POST_ric , dato che fa proprio quello descritto sopra
    //POST_ric=(se esiste su un cammino di albero(r->left)un match di P+1,allora, restituisce una lista concatenata con dimP-1 nodi ciascuno dei quali punta ad un nodo di albero(r->left) che partecipa al match trovato) &&(altrimenti restituisce 0)
2)
    if(match(r->right,P+1,dimP-1) && r->info == *P) return new nodo(r,match(r->right,P+1,dimP-1)
        Sto matchando un elemento, e il prossimo match è a destra, quindi creo un nodo che ha come info il nodo corrente e come next il prossimo match che sarà a destra
    //PRE_ric=(albero(r->right)ben formato, P+1 ha dimP-1 elementi con dimP>1)

        Pre_ric --> POST_ric , dato che fa proprio quello descritto sopra
    //POST_ric=(se esiste su un cammino di albero(r->right)un match di P+1,allora, restituisce una lista concatenata con dimP-1 nodi ciascuno dei quali punta ad un nodo di albero(r->right) che partecipa al match trovato) &&(altrimenti restituisce 0)

3)
    if(match(r->left,P,dimP) && r->info != *P) return match(r->left,P,dimP)
        Non ho matchato l'elemento corrente, e il prossimo match è a sinistra, quindi scorro l'abero a sinistra
    //PRE_ric=(albero(r->left)ben formato, P ha dimP elementi con dimP>0)

        Pre_ric --> POST_ric , dato che fa proprio quello descritto sopra
    //POST_ric=(se esiste su un cammino di albero(r->left)un match di P,allora, restituisce una lista concatenata con dimP nodi ciascuno dei quali punta ad un nodo di albero(r->left) che partecipa al match trovato) &&(altrimenti restituisce 0)

4)
    if(match(r->right,P,dimP) && r->info != *P) return match(r->right,P,dimP)
        Non ho matchato l'elemento corrente, e il prossimo match è a destra, quindi scorro l'abero a destra
    //PRE_ric=(albero(r->right)ben formato, P ha dimP elementi con dimP>0)

        Pre_ric --> POST_ric , dato che fa proprio quello descritto sopra
    //POST_ric=(se esiste su un cammino di albero(r->right)un match di P,allora, restituisce una lista concatenata con dimP nodi ciascuno dei quali punta ad un nodo di albero(r->right) che partecipa al match trovato) &&(altrimenti restituisce 0)

--- FINE DIMOSTRAZIONE INDUTTIVA */